perm filename FIRST.XGP[W79,JMC] blob
sn#429576 filedate 1979-04-02 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1
␈↓ α∧␈↓α1. Introduction and Motivation.
␈↓ α∧␈↓␈↓ αTThis␈αpaper␈αadvances␈αtwo␈αaspects␈αof␈αthe␈αstudy␈αof␈αthe␈αproperties␈αof␈αcomputer␈αprograms␈α-␈αthe
␈↓ α∧␈↓scientifically␈α
motivated␈α
search␈α
for␈α
general␈αtheorems␈α
that␈α
permit␈α
deducing␈α
properties␈α
of␈αprograms
␈↓ α∧␈↓and␈α∩the␈α∩engineering␈α∩problem␈α∩of␈α∩replacing␈α∩debugging␈α∩by␈α∩computer-assisted␈α∩computer-checked
␈↓ α∧␈↓proofs␈α∂that␈α∂programs␈α∞have␈α∂desired␈α∂properties.␈α∞ Both␈α∂tasks␈α∂require␈α∞mathematics,␈α∂but␈α∂the␈α∞second
␈↓ α∧␈↓also␈α
requires␈α
keeping␈α
a␈α
non-mathematical␈α
goal␈αin␈α
mind␈α
-␈α
getting␈α
short␈α
completely␈α
formal␈αproofs
␈↓ α∧␈↓that are easy to write and check by computer.
␈↓ α∧␈↓␈↓ αTA␈α⊂pure␈α⊂Lisp␈α⊂style␈α⊂recursive␈α⊂program␈α⊂␈↓↓P␈↓␈α⊂defines␈α⊂a␈α⊂partial␈α⊂function␈α⊂␈↓↓f␈↓βP␈↓.␈α⊂ By␈α⊃adjoining␈α⊂an
␈↓ α∧␈↓undefined␈αelement␈α␈↓πT␈↓␈α(read␈α"bottom")␈αto␈αthe␈αdata␈αdomains,␈α␈↓↓f␈↓βP␈↓␈αmay␈αbe␈αextended␈αto␈αa␈αtotal␈αfunction
␈↓ α∧␈↓which␈α⊂we␈α⊂denote␈α⊂by␈α⊂the␈α⊂same␈α⊂symbol.␈α⊂ In␈α∂(Cartwright␈α⊂1976),␈α⊂it␈α⊂was␈α⊂shown␈α⊂that␈α⊂␈↓↓f␈↓βP␈↓␈α⊂satisfies␈α∂a
␈↓ α∧␈↓␈↓↓functional␈α∪equation␈↓,␈α∪which␈α∪is␈α∩a␈α∪sentence␈α∪in␈α∪a␈α∪first␈α∩order␈α∪theory␈α∪␈↓↓T␈↓βP␈↓.␈α∪ Besides␈α∪the␈α∩functional
␈↓ α∧␈↓equation,␈α∪␈↓↓T␈↓βP␈↓␈α∩contains␈α∪symbols␈α∪for␈α∩the␈α∪basic␈α∩functions,␈α∪predicates␈α∪and␈α∩constants␈α∪of␈α∪the␈α∩data
␈↓ α∧␈↓domain,␈αaxioms␈αfor␈αthe␈αdata␈αdomain␈αand␈αits␈αextension␈αby␈α␈↓πT␈↓,␈αand␈αadditional␈αfunction␈αsymbols␈αfor
␈↓ α∧␈↓the␈α
functions␈α
defined␈α
by␈αrecursive␈α
programs.␈α
(Cartwright␈α
1976)␈αalso␈α
showed␈α
how␈α
the␈αfunctional
␈↓ α∧␈↓equation␈αcan␈αbe␈α
used␈αto␈αprove␈α
facts␈αabout␈αthe␈α
program␈αby␈αreasoning␈α
within␈α␈↓↓T␈↓βP␈↓,␈αincluding␈αthe␈α
fact
␈↓ α∧␈↓that ␈↓↓f␈↓βP␈↓ is total, i.e. doesn't take the value ␈↓πT␈↓ except when ␈↓πT␈↓ is an argument.
␈↓ α∧␈↓␈↓ αTWhen␈α∀␈↓↓f␈↓βP␈↓␈α∀is␈α∀total,␈α∀and␈α∀sometimes␈α∀when␈α∀it␈α∀isn't,␈α∀it␈α∀is␈α∀completely␈α∀characterized␈α∀by␈α∪the
␈↓ α∧␈↓functional␈α
equation.␈α Otherwise,␈α
the␈α
characterization␈αcan␈α
be␈α
completed␈αby␈α
a␈α
␈↓↓minimization␈αschema␈↓
␈↓ α∧␈↓(McCarthy␈α1978␈αand␈α
this␈αpaper)␈αor␈α
alternatively␈αby␈αa␈α␈↓↓complete␈α
recursive␈αfunction␈↓␈αas␈α
first␈αdefined
␈↓ α∧␈↓in␈α(Cartwright␈α1978).␈α Moreover,␈αwe␈αshow␈αhow␈αto␈αfind␈αa␈αrepresentation␈αof␈α␈↓↓f␈↓βP␈↓␈αby␈αa␈αsentence␈αof␈αthe
␈↓ α∧␈↓form ␈↓↓(∀x)(y = f␈↓βP␈↓↓(x) ≡ A(x))␈↓ where ␈↓↓A(x)␈↓ is a wff of ␈↓↓T␈↓βP␈↓ not involving ␈↓↓f␈↓βP␈↓.
␈↓ α∧␈↓␈↓ αTNow␈αassume␈αthat␈α␈↓↓T␈↓βP␈↓␈α
contains␈αfunctions␈αsufficient␈αfor␈α
axiomatizing␈αbasic␈αsyntax,␈αe.g.␈αLisp␈α
or
␈↓ α∧␈↓elementary␈α
number␈α
theory,␈α
and␈αlet␈α
␈↓↓S␈↓␈α
be␈α
a␈αsentence␈α
of␈α
␈↓↓T␈↓βP␈↓␈α
involving␈αonly␈α
␈↓↓f␈↓βP␈↓␈α
and␈α
the␈αbasic␈α
functions
␈↓ α∧␈↓of␈α
the␈αdata␈α
domain.␈α
Then␈α(Cartwright␈α
and␈α
McCarthy␈α1979)␈α
shows␈α
how␈αto␈α
construct␈α
a␈αsentence␈α
␈↓↓S'␈↓
␈↓ α∧␈↓involving␈αonly␈αthe␈αbasic␈αfunctions␈αof␈αthe␈αdata␈αdomain␈αsuch␈αthat␈αwe␈αcan␈αprove␈αin␈αfirst␈αorder␈αlogic
␈↓ α∧␈↓that␈α
␈↓↓S ≡ S'␈↓.␈α
Therefore,␈α
the␈α
fact␈α
that␈α
total␈α∞correctness␈α
is␈α
not␈α
axiomatizable␈α
in␈α
first␈α
order␈α∞logic␈α
is
␈↓ α∧␈↓just␈αa␈αmatter␈αof␈αthe␈αG␈↓
:␈↓odelian␈αincompleteness␈αof␈αthe␈αdata␈αdomain,␈αand␈αit␈αcan␈αbe␈αexpected␈αthat␈αall
␈↓ α∧␈↓"ordinary"␈α
facts␈αabout␈α
programs␈α
will␈αbe␈α
provable␈α
just␈αas␈α
all␈α
"ordinary"␈αfacts␈α
of␈αelementary␈α
number
␈↓ α∧␈↓theory are provable in spite of its incompleteness.
␈↓ α∧␈↓␈↓ αTThis␈α∩paper␈α∩is␈α∩primarily␈α∩concerned␈α∪with␈α∩proving␈α∩such␈α∩"ordinary"␈α∩facts␈α∪about␈α∩recursive
␈↓ α∧␈↓function␈αprograms␈αwith␈αa␈αview␈αto␈αdeveloping␈αpractical␈αtechniques␈αfor␈αprogram␈α
verification␈αusing
␈↓ α∧␈↓interactive␈α∞theorem␈α∞provers.␈α∞ As␈α∞such␈α∞it␈α∞should␈α∞be␈α∞compared␈α∞with␈α∞other␈α∞ways␈α∞of␈α∞using␈α∂logic␈α∞in
␈↓ α∧␈↓program proving.
␈↓ α∧␈↓␈↓ αTAxiomatizing␈α∩programs␈α∩as␈α∩functions␈α⊃compares␈α∩favorably␈α∩with␈α∩Floyd-Hoare␈α∩methods␈α⊃in
␈↓ α∧␈↓several␈α
respects.␈α
First␈α∞it␈α
permits␈α
stating␈α
and␈α∞proving␈α
facts␈α
that␈α
cannot␈α∞even␈α
be␈α
stated␈α∞in␈α
Floyd-
␈↓ α∧␈↓Hoare␈αformalisms␈αsuch␈αas␈αequivalence␈αof␈αprograms␈αand␈αalgebraic␈αrelations␈αbetween␈αthe␈αfunctions
␈↓ α∧␈↓defined␈α
by␈α
programs.␈α
It␈α
has␈α
the␈αadvantage␈α
compared␈α
to␈α
the␈α
Scott-Strachey␈α
formalisms␈α
that␈αit␈α
uses
␈↓ α∧␈↓ordinary␈αfirst␈α
order␈αlogic␈α
rather␈αthan␈α
a␈αlogic␈αof␈α
continuous␈αfunctions.␈α
This␈αpermits␈α
the␈αuse␈αof␈α
any
␈↓ α∧␈↓mathematical␈α∩facts␈α∩that␈α∩can␈α∩be␈α∩expressed␈α∩in␈α∩first␈α∩order␈α∩logic,␈α∩including␈α∩those␈α∩that␈α∪are␈α∩most
␈↓ α∧␈↓conveniently␈αexpressed␈αin␈αset␈αtheory.␈α This␈αis␈αespecially␈αimportant␈αwhen␈αthe␈αstatement␈αof␈αprogram
␈↓ ↓H␈↓␈↓ 92
␈↓ ↓H␈↓correctness␈αor␈α
its␈αinformal␈α
proof␈αinvolve␈α
other␈αmathematical␈αobjects␈α
than␈αthose␈α
that␈αoccur␈α
in␈αthe
␈↓ ↓H␈↓program data domain.
␈↓ ↓H␈↓␈↓ α_After␈α⊂an␈α⊂informal␈α⊂introduction␈α⊂to␈α⊂recursive␈α⊂programs,␈α⊂subsequent␈α⊂sections␈α⊂of␈α⊃this␈α⊂paper
␈↓ ↓H␈↓discuss␈αthe␈αuse␈αof␈αconditional␈α
expressions␈αand␈αfirst␈αorder␈αlambdas␈α
in␈αfirst␈αorder␈αlogic,␈αadjoining␈α
␈↓πT␈↓
␈↓ ↓H␈↓to␈α⊂the␈α⊂data␈α⊃domains␈α⊂in␈α⊂order␈α⊃to␈α⊂convert␈α⊂partial␈α⊂functions␈α⊃and␈α⊂predicates␈α⊂into␈α⊃total␈α⊂functions,
␈↓ ↓H␈↓axioms␈αfor␈αLisp␈αand␈α
the␈αintegers,␈αthe␈αrepresentation␈α
of␈αrecursive␈αprograms␈αby␈αfunctions,␈α
inductive
␈↓ ↓H␈↓methods␈α∃of␈α∃proof,␈α∃the␈α∃minimization␈α∃schema,␈α∃an␈α∃extended␈α∃example␈α∃of␈α∃a␈α⊗correctness␈α∃proof,
␈↓ ↓H␈↓representation␈α
of␈α
the␈α
inductive␈α
assertion␈α
and␈α
subgoal␈α
induction␈α
methods␈α
as␈α
axiom␈α
schemata,␈αand␈α
a
␈↓ ↓H␈↓convenient way of representing recursively defined functions by non-recursive sentences.
␈↓ ↓H␈↓␈↓ α_Our␈α∃methods␈α∃apply␈α∃directly␈α∃to␈α∃proving␈α∃only␈α∃␈↓↓extensional␈↓␈α∃properties␈α∃of␈α⊗programs,␈α∃e.g.
␈↓ ↓H␈↓properties␈αof␈αthe␈αfunction␈αdefined␈αby␈αthe␈αprogram.␈α Intensional␈αproperties␈αsuch␈αas␈αthe␈αnumber␈αof
␈↓ ↓H␈↓times␈α
an␈αoperation␈α
like␈α
recursion␈αor␈α
␈↓↓cons␈↓␈α
is␈αperformed␈α
are␈α
often␈αextensional␈α
properties␈α
of␈αsimply
␈↓ ↓H␈↓obtained␈α∪␈↓↓derived␈α∪programs␈↓.␈α∪ Some␈α∪of␈α∪these␈α∪properties␈α∪are␈α∪also␈α∪extensional␈α∪properties␈α∪of␈α∪the
␈↓ ↓H␈↓functional of which the function is the least fixed point.
␈↓ ↓H␈↓␈↓ α_An␈α
adequate␈α
background␈α
for␈α
this␈α
paper␈α
is␈α
contained␈α
in␈α
(Manna␈α
1974)␈α
and␈α
more␈α
concisely␈α
in
␈↓ ↓H␈↓(Manna,␈α∂Ness␈α∞and␈α∂Vuillemin␈α∞1973).␈α∂ The␈α∞connections␈α∂of␈α∞recursive␈α∂programs␈α∞with␈α∂second␈α∞order
␈↓ ↓H␈↓logic␈αare␈α
given␈αin␈α(Cooper␈α
1969)␈αand␈α(Park␈α
1970).␈α Our␈α
notation␈αdiffers␈αfrom␈α
Manna's␈αin␈αorder␈α
to
␈↓ ↓H␈↓use the = sign exactly as in first order logic.
␈↓ ↓H␈↓α2. Recursive Programs.
␈↓ ↓H␈↓␈↓ α_We consider recursive programs like
␈↓ ↓H␈↓␈↓↓Factorial:␈↓ αxn! ← ␈↓αif␈↓↓ n equal 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ n . (n - 1)!␈↓
␈↓ ↓H␈↓which␈α∂is␈α∞the␈α∂well␈α∂known␈α∞recursive␈α∂program␈α∂for␈α∞the␈α∂factorial␈α∂function.␈α∞ We␈α∂will␈α∂use␈α∞capitalized
␈↓ ↓H␈↓italic␈α∂names␈α∞for␈α∂programs␈α∞themselves␈α∂regarded␈α∂as␈α∞texts␈α∂and␈α∞the␈α∂corresponding␈α∂name␈α∞initialized
␈↓ ↓H␈↓with␈α
lower␈α
case␈αas␈α
a␈α
name␈αfor␈α
the␈α
function␈αcomputed␈α
by␈α
the␈αprogram,␈α
except␈α
that␈αas␈α
in␈α
the␈αcase␈α
of
␈↓ ↓H␈↓␈↓↓Factorial,␈↓␈α
we␈α
sometimes␈α
use␈α
an␈α
infix␈αor␈α
other␈α
conventional␈α
notation␈α
for␈α
the␈α
function.␈α Mutually
␈↓ ↓H␈↓recursive sets of function programs will also be considered.
␈↓ ↓H␈↓␈↓ α_Another␈αexample␈αis␈αthe␈αLisp␈αprogram␈α␈↓↓Append␈↓.␈α In␈αthis␈αpaper␈αwe␈αwill␈αuse␈αthe␈αLisp␈αexternal
␈↓ ↓H␈↓or␈αpublication␈αnotation␈α
of␈α(McCarthy␈αand␈α
Talcott␈α1979),␈αand␈αwe␈α
will␈αwrite␈α␈↓↓u*v␈↓␈α
for␈α␈↓↓append[u,v]␈↓.
␈↓ ↓H␈↓We then have
␈↓ ↓H␈↓␈↓↓Append:␈↓ αxu * v ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓.
␈↓ ↓H␈↓Here␈α
we␈α
are␈α
using␈α
␈↓αn␈↓␈α
for␈α
␈↓↓null,␈↓␈α
␈↓αa␈↓␈α
for␈α
␈↓↓car,␈↓␈α
␈↓αd␈↓␈α
for␈α
␈↓↓cdr␈↓␈α
and␈α
an␈α
infixed␈α
.␈α
for␈α
␈↓↓cons.␈↓␈α
We␈α
omit␈αbrackets␈α
for
␈↓ ↓H␈↓functions of one argument. In a more traditional Lisp M-expression notation we would have
␈↓ ↓H␈↓␈↓ α_␈↓↓append[u,v] ← ␈↓αif␈↓↓ null[u] ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ cons[car[u], append[cdr[u], v]]␈↓,
␈↓ ↓H␈↓and in Maclisp S-expression notation, this would be
␈↓ α∧␈↓␈↓ u3
␈↓ α∧␈↓␈↓ αt(DEFUN APPEND (U V)
␈↓ α∧␈↓␈↓ β4(COND ((NULL U) V) (T (CONS (CAR U) (APPEND (CDR U) V))))).
␈↓ α∧␈↓␈↓ αTOur␈α
objective␈α
is␈α∞to␈α
prove␈α
facts␈α∞about␈α
such␈α
recursively␈α∞defined␈α
functions␈α
by␈α∞regarding␈α
the
␈↓ α∧␈↓recursive␈α
function␈αdefinitions␈α
as␈αsentences␈α
of␈αfirst␈α
order␈αlogic.␈α
More␈αaccurately,␈α
we␈α
represent␈αthe
␈↓ α∧␈↓recursive␈αfunction␈αdefinitions␈αby␈αvery␈αsimilar␈αsentences␈αof␈αfirst␈αorder␈αlogic.␈α ␈↓↓Factorial␈↓␈αand␈α
␈↓↓Append␈↓
␈↓ α∧␈↓are translated into the sentences
␈↓ α∧␈↓1)␈↓ αt ␈↓↓(∀n)(iseint n ⊃ n! = ␈↓αif␈↓↓ n equal 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ n ␈↓πx␈↓↓ (n - 1)!)␈↓
␈↓ α∧␈↓and
␈↓ α∧␈↓2)␈↓ αt ␈↓↓(∀u v)(iselist u ∧ iselist v ⊃ u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v])␈↓
␈↓ α∧␈↓respectively.␈α The␈αform␈αof␈αconditional␈αexpression␈α␈↓↓␈↓αif␈↓↓␈αp␈α␈↓αthen␈↓↓␈αa␈α␈↓αelse␈↓↓␈αb␈↓␈αused␈αin␈αthese␈αsentences␈αis␈αjust
␈↓ α∧␈↓a function that could as well be written ␈↓↓if(p,a,b)␈↓ so far as the logic is concerned.
␈↓ α∧␈↓␈↓ αTThe␈αpredicates␈α␈↓↓iseint␈↓␈αand␈α
␈↓↓iselist␈↓␈αrespectively␈αrestrict␈αtheir␈α
arguments␈αto␈αbe␈αextended␈α
integers
␈↓ α∧␈↓(i.e.␈α⊃the␈α∩integers␈α⊃extended␈α⊃by␈α∩␈↓πT␈↓)␈α⊃and␈α⊃extended␈α∩lists.␈α⊃ When␈α⊃these␈α∩domains␈α⊃can␈α⊃be␈α∩taken␈α⊃for
␈↓ α∧␈↓granted, we can omit the explicit restrictions and write
␈↓ α∧␈↓3)␈↓ αt ␈↓↓(∀n)(n! = ␈↓αif␈↓↓ n equal 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ n ␈↓πx␈↓↓ (n - 1)!)␈↓
␈↓ α∧␈↓and
␈↓ α∧␈↓4)␈↓ αt ␈↓↓(∀u v)(u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v])␈↓
␈↓ α∧␈↓␈↓ αTThe␈α∂sentences␈α∂(1)␈α∂and␈α∂(2)␈α⊂completely␈α∂characterize␈α∂the␈α∂functions␈α∂defined␈α∂by␈α⊂the␈α∂programs
␈↓ α∧␈↓␈↓↓Factorial␈↓␈αand␈α␈↓↓Append,␈↓␈αso␈α
proofs␈αof␈αthe␈αproperties␈αof␈α
these␈αfunctions␈αcan␈αbe␈αdeduced␈α
from␈αthese
␈↓ α∧␈↓sentences␈α∃together␈α∃with␈α∀axioms␈α∃characterizing␈α∃the␈α∃natural␈α∀number␈α∃and␈α∃Lisp␈α∃data␈α∀domains
␈↓ α∧␈↓respectively. For example, suppose we wish to prove that * satisfies the equations
␈↓ α∧␈↓5)␈↓ αt ␈↓↓(∀v)(␈↓NIL␈↓↓ * v = v)␈↓
␈↓ α∧␈↓and
␈↓ α∧␈↓6)␈↓ αt ␈↓↓(∀u)(u * ␈↓NIL␈↓↓ = u)␈↓,
␈↓ α∧␈↓i.e.␈α∪NIL␈α∩is␈α∪both␈α∪a␈α∩left␈α∪and␈α∪right␈α∩identity␈α∪for␈α∪the␈α∩*␈α∪operation.␈α∪ (5)␈α∩is␈α∪trivially␈α∪obtained␈α∩by
␈↓ α∧␈↓substituting␈α
NIL␈αfor␈α
␈↓↓u␈↓␈αin␈α
(1)␈α
and␈αusing␈α
the␈αrules␈α
for␈α
evaluating␈αconditional␈α
expressions␈αwhich␈α
will
␈↓ α∧␈↓have␈α∞been␈α∞added␈α∞to␈α∞the␈α∂usual␈α∞rules␈α∞for␈α∞first␈α∞order␈α∂logic.␈α∞ (6)␈α∞expresses␈α∞a␈α∞more␈α∂typical␈α∞program
␈↓ α∧␈↓property in that its proof requires a mathematical induction.
␈↓ α∧␈↓This induction is accomplished by substituting
␈↓ α∧␈↓7)␈↓ αt ␈↓↓␈↓ F␈↓↓(u) ≡ (u * ␈↓NIL␈↓↓ = u)␈↓
␈↓ ↓H␈↓␈↓ 94
␈↓ ↓H␈↓in the list induction schema
␈↓ ↓H␈↓8)␈↓ α8 ␈↓↓␈↓ F␈↓↓(␈↓NIL␈↓↓) ∧ (∀u)(islist u ∧ ¬null u ∧ ␈↓ F␈↓↓(␈↓αd␈↓↓ u) ⊃ ␈↓ F␈↓↓(u)) ⊃ (∀u)(islist u ⊃ ␈↓ F␈↓↓(u))␈↓,
␈↓ ↓H␈↓and␈α
using␈α(2),␈α
the␈αaxioms␈α
for␈α
lists,␈αand␈α
the␈αrules␈α
of␈α
inference␈αof␈α
first␈αorder␈α
logic␈α
including␈αthose
␈↓ ↓H␈↓for conditional expressions.
␈↓ ↓H␈↓␈↓ α_Once␈αthe␈α
formalism␈αhas␈α
been␈αestablished,␈α
totality␈αcan␈α
be␈αproved␈α
in␈αthe␈α
same␈αway␈α
as␈αother
␈↓ ↓H␈↓properties of the programs. Thus the totality of ␈↓↓u*v␈↓ is proved by substituting
␈↓ ↓H␈↓9)␈↓ α8 ␈↓↓␈↓ F␈↓↓(u) ≡ islist[u*v]␈↓
␈↓ ↓H␈↓into the schema (8) and using (2), etc. as described above.
␈↓ ↓H␈↓␈↓ α_The␈α
translation␈α
of␈αthe␈α
program␈α
into␈α
a␈αlogical␈α
sentences␈α
would␈α
be␈αtrivial␈α
to␈α
justify␈α
if␈αwe␈α
were
␈↓ ↓H␈↓always␈α∂assured␈α∂that␈α⊂the␈α∂program␈α∂terminates␈α∂for␈α⊂all␈α∂sets␈α∂of␈α∂arguments␈α⊂and␈α∂thus␈α∂defines␈α⊂a␈α∂total
␈↓ ↓H␈↓function.␈α∞ The␈α∞innovation␈α∞is␈α∞that␈α∞the␈α∞translation␈α∞is␈α∞possible␈α∞even␈α∞without␈α∞that␈α∞guarantee␈α∞at␈α
the
␈↓ ↓H␈↓cheap␈α⊃price␈α⊃of␈α⊃extending␈α∩the␈α⊃data␈α⊃domain␈α⊃by␈α∩an␈α⊃undefined␈α⊃element␈α⊃␈↓πT␈↓,␈α∩rewriting␈α⊃recursively
␈↓ ↓H␈↓defined␈α
predicate␈α
programs␈α∞as␈α
function␈α
programs,␈α
having␈α∞two␈α
kinds␈α
of␈α
equality␈α∞and␈α
conditional
␈↓ ↓H␈↓expression,␈α
and␈α
providing␈α
each␈α
predicate␈α
with␈α
two␈α
forms␈α
-␈α
one␈α
a␈α
genuine␈α
predicate␈α
in␈α
the␈α
logic
␈↓ ↓H␈↓and␈α
the␈αother␈α
a␈αfunction␈α
imitating␈α
the␈αpartial␈α
predicate␈αby␈α
a␈α
function␈αthat␈α
takes␈αthe␈α
value␈α␈↓πT␈↓␈α
when
␈↓ ↓H␈↓the␈α
program␈α
for␈α
the␈α
predicate␈α
doesn't␈α
terminate.␈α
Proofs␈α
of␈α
termination␈α
then␈α
take␈α
the␈α
same␈α
form␈α
as
␈↓ ↓H␈↓other␈α⊃inductive␈α∩proofs.␈α⊃ However,␈α∩additional␈α⊃formalism␈α⊃is␈α∩required␈α⊃to␈α∩characterize␈α⊃completely
␈↓ ↓H␈↓programs that don't always terminate.
␈↓ ↓H␈↓␈↓ α_The␈α⊃next␈α⊃sections␈α⊃introduce␈α⊃the␈α⊃logical␈α∩basis␈α⊃of␈α⊃the␈α⊃formalism␈α⊃and␈α⊃axioms␈α∩and␈α⊃axiom
␈↓ ↓H␈↓schemata for Lisp.
␈↓ ↓H␈↓α3. Two Useful Extensions to First Order Logic.
␈↓ ↓H␈↓␈↓ α_We␈α
begin␈α
by␈α
extending␈α
first␈α
order␈α∞logic␈α
to␈α
include␈α
conditional␈α
expressions␈α
and␈α∞first␈α
order
␈↓ ↓H␈↓lambda␈αexpressions.␈α This␈αallows␈αus␈αto␈αparallel␈αthe␈αstructure␈αof␈αrecursive␈αprograms␈αwithin␈αlogical
␈↓ ↓H␈↓sentences.
␈↓ ↓H␈↓␈↓ α_We␈αcannot␈αadd␈αarbitrary␈αprogramming␈α
constructions␈αto␈αfirst␈αorder␈αlogic␈αwithout␈α
risking␈αits
␈↓ ↓H␈↓useful␈α∩properties␈α∩such␈α∩as␈α∩completeness␈α⊃or␈α∩even␈α∩consistency.␈α∩ Fortunately,␈α∩these␈α∩extensions␈α⊃are
␈↓ ↓H␈↓harmless,␈α
because␈α
they␈α∞are␈α
not␈α
merely␈α∞conservative;␈α
they␈α
can␈α
even␈α∞be␈α
eliminated␈α
from␈α∞wffs,␈α
and
␈↓ ↓H␈↓they␈αare␈αgenerally␈αuseful.␈α In␈αfact,␈αthey␈αare␈αuseful␈αfor␈αexpressing␈αmathematical␈αideas␈αconcisely␈αand
␈↓ ↓H␈↓understandably␈α⊃quite␈α⊂apart␈α⊃from␈α⊂applications␈α⊃to␈α⊂computer␈α⊃science.␈α⊂ The␈α⊃reader␈α⊂is␈α⊃assumed␈α⊂to
␈↓ ↓H␈↓know␈α∂about␈α∂first␈α∂order␈α∂logic,␈α⊂conditional␈α∂expressions␈α∂and␈α∂lambda␈α∂expressions;␈α∂we␈α⊂explain␈α∂only
␈↓ ↓H␈↓their connection.
␈↓ ↓H␈↓␈↓ α_Remember␈α
that␈αthe␈α
syntax␈αof␈α
first␈αorder␈α
logic␈αis␈α
given␈αin␈α
the␈αform␈α
of␈αinductive␈α
rules␈αfor␈α
the
␈↓ ↓H␈↓formation of terms and wffs. The rule for forming terms is extended as follows:
␈↓ α∧␈↓␈↓ u5
␈↓ α∧␈↓␈↓ αTIf␈α
␈↓↓P␈↓␈α
is␈α
a␈α∞wff␈α
and␈α
␈↓↓a␈↓␈α
and␈α∞␈↓↓b␈↓␈α
are␈α
terms,␈α
then␈α∞␈↓↓IF␈α
P␈α
THEN␈α
a␈α∞ELSE␈α
b␈↓␈α
is␈α
a␈α∞term.␈α
Sometimes
␈↓ α∧␈↓parentheses␈αmust␈αbe␈αadded␈αto␈αinsure␈αunique␈αdecomposition.␈α Note␈αthat␈αthis␈αmakes␈αthe␈αdefinitions
␈↓ α∧␈↓of term and wff mutually recursive.
␈↓ α∧␈↓␈↓ αTThe␈α⊂semantics␈α⊂of␈α⊂conditional␈α⊃expression␈α⊂terms␈α⊂is␈α⊂given␈α⊃by␈α⊂a␈α⊂rule␈α⊂for␈α⊃determining␈α⊂their
␈↓ α∧␈↓values.␈α⊂ Namely,␈α⊂if␈α⊂␈↓↓P␈↓␈α⊃is␈α⊂true,␈α⊂then␈α⊂the␈α⊂value␈α⊃of␈α⊂␈↓↓IF␈α⊂P␈α⊂THEN␈α⊂a␈α⊃ELSE␈α⊂b␈↓␈α⊂is␈α⊂the␈α⊂value␈α⊃of␈α⊂␈↓↓a.␈↓
␈↓ α∧␈↓Otherwise it is the value of ␈↓↓b.␈↓
␈↓ α∧␈↓␈↓ αTIt␈α∪is␈α∪also␈α∪necessary␈α∪to␈α∪add␈α∪rules␈α∪of␈α∪inference␈α∪to␈α∪the␈α∪logic␈α∪concerned␈α∪with␈α∩conditional
␈↓ α∧␈↓expressions.␈α∞ One␈α∂could␈α∞get␈α∂by␈α∞with␈α∞rules␈α∂permitting␈α∞the␈α∂elimination␈α∞of␈α∂conditional␈α∞expressions
␈↓ α∧␈↓from␈α∂sentences␈α∞and␈α∂their␈α∞introduction.␈α∂ These␈α∞rules␈α∂are␈α∞important␈α∂anyway,␈α∞because␈α∂they␈α∞permit
␈↓ α∧␈↓proof␈α⊂of␈α⊂the␈α⊂metatheorem␈α⊃that␈α⊂the␈α⊂main␈α⊂properties␈α⊂of␈α⊃first␈α⊂order␈α⊂logic␈α⊂are␈α⊂unaffected␈α⊃by␈α⊂the
␈↓ α∧␈↓addition␈α∩of␈α⊃conditional␈α∩expressions.␈α∩ These␈α⊃include␈α∩completeness,␈α⊃the␈α∩deduction␈α∩theorem,␈α⊃and
␈↓ α∧␈↓semi-decidability.
␈↓ α∧␈↓␈↓ αTIn␈α
order␈α
to␈α
state␈α
these␈α
rules␈α
it␈α
is␈α
convenient␈α
to␈α
introduce␈α
conditional␈α
expressions␈α
also␈α∞as␈α
a
␈↓ α∧␈↓ternary␈αlogical␈αconnective.␈α A␈α
more␈αfastidious␈αexposition␈αwould␈α
use␈αa␈αdifferent␈αnotation␈αfor␈α
logical
␈↓ α∧␈↓conditional␈αexpressions,␈αbut␈αwe␈α
will␈αuse␈αthem␈αso␈α
little␈αthat␈αwe␈αmight␈α
as␈αwell␈αuse␈αthe␈αsame␈α
notation,
␈↓ α∧␈↓especially␈αsince␈αit␈αis␈αnot␈αambiguous.␈α Namely,␈αif␈α␈↓↓P,␈↓␈α␈↓↓Q,␈↓␈α
and␈α␈↓↓R␈↓␈αare␈αwffs,␈αthen␈αso␈αis␈α␈↓↓IF␈αP␈αTHEN␈α
Q
␈↓ α∧␈↓↓ELSE␈α⊃R␈↓.␈α⊂ Its␈α⊃semantics␈α⊂is␈α⊃given␈α⊂by␈α⊃considering␈α⊂it␈α⊃as␈α⊂a␈α⊃synonym␈α⊂for␈α⊃␈↓↓((P␈α⊂∧␈α⊃Q)␈α⊂∨␈α⊃(¬P␈α⊃∧␈α⊂R))␈↓.
␈↓ α∧␈↓Elimination of conditional expressions is made possible by the distributive laws
␈↓ α∧␈↓10)␈↓ αt ␈↓↓f(IF P THEN a ELSE b) = IF P THEN f(a) ELSE f(b)␈↓
␈↓ α∧␈↓and
␈↓ α∧␈↓11)␈↓ αt␈↓ αt␈↓↓␈↓ F␈↓↓(IF P THEN a ELSE b)␈↓ ¬t≡ IF P THEN ␈↓ F␈↓↓(a) ELSE ␈↓ F␈↓↓(b)␈↓
␈↓ α∧␈↓␈↓ ¬t≡ ␈↓↓(P ∧ ␈↓ F␈↓↓(a)) ∨ (¬P ∧ ␈↓ F␈↓↓(b))␈↓
␈↓ α∧␈↓where ␈↓↓f␈↓ and ␈↓ F␈↓ stand for arbitrary function and predicate symbols respectively.
␈↓ α∧␈↓␈↓ αTNotice␈α
that␈α
this␈αaddition␈α
to␈α
the␈αlogic␈α
has␈α
nothing␈αto␈α
do␈α
with␈αpartial␈α
functions␈α
or␈αthe␈α
element
␈↓ α∧␈↓␈↓πT␈↓.
␈↓ α∧␈↓␈↓ αTWhile␈αthe␈αabove␈αrules␈αare␈αsufficient␈αto␈αpreserve␈αthe␈αcompleteness␈αof␈αfirst␈αorder␈αlogic,␈αproofs
␈↓ α∧␈↓are␈α∂often␈α∂greatly␈α⊂shortened␈α∂by␈α∂using␈α⊂the␈α∂additional␈α∂rules␈α⊂introduced␈α∂in␈α∂(McCarthy␈α⊂1963).␈α∂ We
␈↓ α∧␈↓mention␈α
especially␈α
an␈α
extended␈α
form␈α
of␈αthe␈α
rule␈α
for␈α
replacing␈α
an␈α
expression␈α
by␈αanother␈α
expression
␈↓ α∧␈↓proved␈α
equal␈αto␈α
it.␈α Suppose␈α
we␈αwant␈α
to␈αreplace␈α
the␈αexpression␈α
␈↓↓c␈↓␈αby␈α
an␈αexpression␈α
␈↓↓c'␈↓␈α
within␈αthe
␈↓ α∧␈↓conditional␈αexpression␈α␈↓↓IF␈αP␈αTHEN␈αa␈αELSE␈αb␈↓.␈α To␈αreplace␈αan␈αoccurrence␈αof␈α␈↓↓c␈↓␈αwithin␈α␈↓↓a,␈↓␈αwe␈α
need
␈↓ α∧␈↓not␈α
prove␈α␈↓↓c = c'␈↓␈α
but␈α
merely␈α␈↓↓P ⊃ c = c'␈↓.␈α
Likewise␈α
if␈αwe␈α
want␈α
to␈αreplace␈α
an␈α
occurrence␈αof␈α
␈↓↓c␈↓␈α
in␈α␈↓↓b,␈↓␈α
we
␈↓ α∧␈↓need only prove ␈↓↓¬P ⊃ c = c'␈↓. This principle is further extended in the afore-mentioned paper.
␈↓ α∧␈↓␈↓ αTA␈α⊃further␈α⊂useful␈α⊃and␈α⊂eliminable␈α⊃extension␈α⊂to␈α⊃the␈α⊂logic␈α⊃is␈α⊂to␈α⊃allow␈α⊂"first␈α⊃order"␈α⊂lambda
␈↓ α∧␈↓expressions␈α∂as␈α∂function␈α∂and␈α∂predicate␈α∂expressions.␈α∂ Thus␈α∞if␈α∂␈↓↓x␈↓␈α∂is␈α∂an␈α∂individual␈α∂variable,␈α∂␈↓↓e␈↓␈α∂is␈α∞a
␈↓ α∧␈↓term,␈αand␈α␈↓↓P␈↓␈αis␈αa␈αwff,␈αthen␈α␈↓↓(λx)e␈↓␈αand␈α␈↓↓(λx)P␈↓␈αmay␈αbe␈αused␈αwherever␈αa␈αfunction␈αsymbol␈αor␈αpredicate
␈↓ α∧␈↓symbol␈αrespectively␈αare␈α
allowed.␈α Formally,␈αthis␈αrequires␈α
that␈αthe␈αsyntactic␈αcategories␈α
of␈α<function
␈↓ ↓H␈↓␈↓ 96
␈↓ ↓H␈↓symbol>␈α↔and␈α↔<predicate␈α_symbol>␈α↔be␈α↔generalized␈α_to␈α↔<function␈α↔expression>␈α_and␈α↔<predicate
␈↓ ↓H␈↓expression>␈α
respectively␈α
and␈αthat␈α
these␈α
categories␈α
are␈αthen␈α
defined␈α
mutually␈α
recursively␈αwith␈α
terms
␈↓ ↓H␈↓and wffs.
␈↓ ↓H␈↓␈↓ α_The␈α∀only␈α∀inference␈α∀rule␈α∀required␈α∀is␈α∪lambda␈α∀conversion␈α∀which␈α∀serves␈α∀to␈α∀eliminate␈α∪or
␈↓ ↓H␈↓introduce␈αlambda␈αexpressions.␈α According␈αto␈αthis␈αrule,␈αa␈αwff␈αis␈αequivalent␈αto␈αa␈αwff␈αobtained␈αfrom
␈↓ ↓H␈↓it␈αby␈αreplacing␈αa␈αsub-wff␈αor␈αsub-term␈αby␈αone␈αobtained␈αfrom␈αit␈αby␈αlambda␈αconversion.␈α The␈αrules
␈↓ ↓H␈↓for␈αlambda␈α
conversion␈αmust␈αinclude␈α
alphabetic␈αchanges␈α
of␈αbound␈αvariables␈α
when␈αneeded␈αto␈α
avoid
␈↓ ↓H␈↓capture of the free variables in arguments of lambda expressions.
␈↓ ↓H␈↓␈↓ α_The␈α∞use␈α∞of␈α∞minimization␈α
schemata␈α∞and␈α∞schemata␈α∞of␈α
induction␈α∞is␈α∞facilitated␈α∞by␈α∞first␈α
order
␈↓ ↓H␈↓lambda␈αexpressions,␈αsince␈αthe␈α
substitution␈αjust␈αreplaces␈αoccurrences␈α
of␈αthe␈αfunction␈αvariable␈αin␈α
the
␈↓ ↓H␈↓schema␈α⊂by␈α⊃a␈α⊂lambda␈α⊃expression␈α⊂which␈α⊂can␈α⊃subsequently␈α⊂be␈α⊃expanded␈α⊂by␈α⊃lambda␈α⊂conversion.
␈↓ ↓H␈↓Using␈αlambda␈α
expressions␈αsomewhat␈α
simplifies␈αthe␈αrule␈α
for␈αsubstitution␈α
in␈αschemata.␈α
First␈αorder
␈↓ ↓H␈↓lambda␈αexpressions␈αalso␈αpermit␈αmany␈αsentences␈αto␈αbe␈αexpressed␈αmore␈αcompactly␈αand␈αmay␈αbe␈αused
␈↓ ↓H␈↓to␈α∞avoid␈α∞duplicate␈α∞computations␈α∞in␈α∞recursive␈α∞programs.␈α∞ Thus␈α∞we␈α∞can␈α∂write␈α∞␈↓↓[(λx)(x␈↓#
2␈↓# + x)](a + b)␈↓
␈↓ ↓H␈↓instead␈α∪of␈α∩␈↓↓(a + b)␈↓#
2␈↓# + (a + b)␈↓.␈α∪ Since␈α∩all␈α∪occurrences␈α∪of␈α∩first␈α∪order␈α∩lambda␈α∪expressions␈α∪can␈α∩be
␈↓ ↓H␈↓eliminated␈α⊃from␈α∩wffs␈α⊃by␈α⊃lambda␈α∩conversion,␈α⊃the␈α∩metatheorems␈α⊃of␈α⊃first␈α∩order␈α⊃logic␈α∩are␈α⊃again
␈↓ ↓H␈↓preserved.␈α∞ The␈α∞reason␈α∂we␈α∞don't␈α∞get␈α∂the␈α∞full␈α∞lambda␈α∂calculus␈α∞is␈α∞that␈α∂the␈α∞syntactic␈α∞rules␈α∂of␈α∞first
␈↓ ↓H␈↓order␈α
logic␈α∞prevent␈α
a␈α∞variable␈α
from␈α
being␈α∞used␈α
in␈α∞both␈α
term␈α
and␈α∞function␈α
positions.␈α∞ While␈α
we
␈↓ ↓H␈↓have␈α
illustrated␈α
the␈α
use␈αof␈α
lambda␈α
expressions␈α
with␈αsingle␈α
variable␈α
λ's,␈α
expressions␈α
like␈α␈↓↓(λx y z)e␈↓
␈↓ ↓H␈↓are␈α
also␈α
useful␈α
and␈α
give␈αno␈α
trouble.␈α
It␈α
is␈α
also␈α
easily␈αseen␈α
that␈α
lambda␈α
conversion␈α
within␈α
a␈αterm
␈↓ ↓H␈↓preserves its value, and lambda conversion within a wff preserves its truth value.
␈↓ ↓H␈↓␈↓ α_Actually␈α
it␈α
seems␈α
that␈α
even␈α
higher␈α
order␈α
λ's␈α
won't␈α
get␈α
us␈α
out␈α
of␈α
first␈α
order␈α
logic␈α
provided
␈↓ ↓H␈↓rules␈α
of␈α
typing␈αare␈α
obeyed␈α
and␈αwe␈α
provide␈α
no␈αway␈α
of␈α
quantifying␈αover␈α
function␈α
variables.␈α Any
␈↓ ↓H␈↓occurrences␈α∞of␈α∞higher␈α∞order␈α
lambda␈α∞expressions␈α∞in␈α∞wffs␈α∞are␈α
eliminable␈α∞just␈α∞by␈α∞carrying␈α∞out␈α
the
␈↓ ↓H␈↓indicated lambda conversions. For example, we could define
␈↓ ↓H␈↓␈↓ α_␈↓↓transitive = (λR)((∀X Y Z)(R(X,Y) ∧ R(Y,Z) ⊃ R(X,Z)))␈↓,
␈↓ ↓H␈↓and any use of ␈↓↓transitive␈↓ in a wff would be eliminable using its definition and lambda conversion.
␈↓ ↓H␈↓α4. Partial Functions and Partial Predicates.
␈↓ ↓H␈↓␈↓ α_The␈αmain␈αdifficulty␈αto␈αbe␈αovercome␈αin␈αrepresenting␈αrecursive␈αprograms␈αby␈αlogical␈αsentences
␈↓ ↓H␈↓is␈α⊂that␈α∂the␈α⊂computation␈α∂of␈α⊂an␈α∂arbitrary␈α⊂recursive␈α∂program␈α⊂cannot␈α∂be␈α⊂guaranteed␈α⊂to␈α∂terminate.
␈↓ ↓H␈↓Consider the recursive program
␈↓ ↓H␈↓␈↓↓Runaway:␈↓ αxf(n) ← f(n) + 1␈↓
␈↓ ↓H␈↓over the integers. If we translate ␈↓↓Runaway␈↓ into the sentence
␈↓ ↓H␈↓12)␈↓ α8 ␈↓↓(∀n)(f(n) = f(n) +1)␈↓
␈↓ α∧␈↓␈↓ u7
␈↓ α∧␈↓and use the axioms of arithmetic, we get a contradiction.
␈↓ α∧␈↓␈↓ αTThe␈α∂way␈α∂out␈α∂is␈α∂to␈α∂adjoin␈α∂to␈α∞our␈α∂data␈α∂domains␈α∂an␈α∂additional␈α∂element␈α∂␈↓πT␈↓␈α∂(read␈α∞"bottom"),
␈↓ α∧␈↓which␈α⊃is␈α⊃taken␈α⊃to␈α⊃be␈α⊃the␈α⊃value␈α⊃of␈α⊃the␈α⊃function␈α⊃when␈α⊃the␈α⊃computation␈α⊃doesn't␈α⊃terminate.␈α⊂ In
␈↓ α∧␈↓addition we add the axiom
␈↓ α∧␈↓13)␈↓ αt ␈↓↓(∀n)(isint(n) ∨ n = ␈↓πT␈↓↓)␈↓,
␈↓ α∧␈↓and␈α⊂modify␈α⊂the␈α⊂axioms␈α⊃for␈α⊂arithmetic␈α⊂to␈α⊂refer␈α⊂to␈α⊃elements␈α⊂satisfying␈α⊂␈↓↓isint␈↓.␈α⊂ Then␈α⊃going␈α⊂from
␈↓ α∧␈↓␈↓↓Runaway␈↓ to (12) doesn't lead to a contradiction but to the desired result that
␈↓ α∧␈↓14)␈↓ αt ␈↓↓(∀n)(f(n) = ␈↓πT␈↓↓)␈↓,
␈↓ α∧␈↓provided we also postulate that
␈↓ α∧␈↓15)␈↓ αt ␈↓↓(∀n)(n + ␈↓πT␈↓↓ = ␈↓πT␈↓↓ + n = ␈↓πT␈↓↓)␈↓,
␈↓ α∧␈↓which␈α⊂is␈α⊂reasonable␈α⊂given␈α⊂the␈α⊂interpretation␈α⊂of␈α∂␈↓πT␈↓␈α⊂as␈α⊂the␈α⊂value␈α⊂of␈α⊂a␈α⊂computation␈α⊂that␈α∂doesn't
␈↓ α∧␈↓terminate.␈α
We␈α
will␈α
postulate␈αthat␈α
all␈α
of␈α
the␈α
base␈αfunctions,␈α
except␈α
the␈α
conditional␈αexpression,␈α
have
␈↓ α∧␈↓␈↓πT␈↓␈α⊂as␈α⊂value␈α⊂if␈α⊂any␈α⊂argument␈α⊂is␈α⊂␈↓πT␈↓.␈α⊂ Such␈α⊂functions␈α⊂are␈α⊂called␈α⊂␈↓↓strict␈↓.␈α⊂ Manna␈α⊂(1974)␈α⊂calls␈α⊂them
␈↓ α∧␈↓␈↓↓natural extensions␈↓ of the functions defined on the domain without ␈↓πT␈↓.
␈↓ α∧␈↓␈↓ αTWe␈αhave␈αdiscussed␈αtreating␈αpartial␈αfunctions␈αby␈αintroducing␈α␈↓πT␈↓.␈α A␈αfunction␈αtakes␈αthe␈αvalue
␈↓ α∧␈↓␈↓πT␈↓␈αwhen␈αthe␈αprogram␈αthat␈αcomputes␈αit␈αdoesn't␈αterminate,␈αand␈αit␈αis␈αsometimes␈αconvenient␈αto␈αgive␈αa
␈↓ α∧␈↓function the value ␈↓πT␈↓ in some other cases when we want it to be undefined.
␈↓ α∧␈↓␈↓ αTIt␈α
is␈α
convenient␈α
to␈α
introduce␈α
a␈α
rather␈α
trivial␈α
partial␈α
ordering␈α
relation␈α
on␈α
our␈α
data␈αdomain
␈↓ α∧␈↓once it has been extended by adjoining ␈↓πT␈↓. Namely, we define the relation ␈↓↓X ␈↓πa␈↓↓ Y␈↓ by
␈↓ α∧␈↓16)␈↓ αt ␈↓↓(∀X Y)(X ␈↓πa␈↓↓ Y ≡ X = ␈↓πT␈↓↓ ∧ Y ≠ ␈↓πT␈↓↓)␈↓.
␈↓ α∧␈↓(Readers␈αof␈α
(Manna␈α1974)␈α
should␈αnote␈α
that␈αthe␈α
symbol␈α≡␈α
is␈αbeing␈α
used␈αin␈α
its␈αcommon␈αlogical␈α
sense
␈↓ α∧␈↓of␈α"if␈α
and␈αonly␈α
if").␈α We␈α
also␈αmake␈α
corresponding␈αdefinitions␈α
of␈α␈↓πc␈↓,␈α
␈↓πb␈↓,␈αand␈α
␈↓πd␈↓.␈α The␈α
ordering␈αcan␈α
be
␈↓ α∧␈↓extended to functions by defining
␈↓ α∧␈↓17)␈↓ αt ␈↓↓f ␈↓πb␈↓↓ g ≡ (∀X)(f(X) ␈↓πb␈↓↓ g(X))␈↓.
␈↓ α∧␈↓This␈α
induced␈α
ordering␈α
is␈α
not␈α
so␈α
trivial,␈α
but␈α
we␈α
don't␈α
use␈α
it␈α
in␈α
this␈α
paper,␈α
since␈α
it␈α
gets␈α
us␈α
out␈αof
␈↓ α∧␈↓first␈αorder␈αlogic.␈α Even␈αthough␈α(16)␈αdefines␈αa␈αrather␈αtrivial␈αordering,␈αwe␈αfind␈αthat␈αit␈αshortens␈αand
␈↓ α∧␈↓clarifies many formulas.
␈↓ α∧␈↓␈↓ αTPartial␈α⊂predicates␈α⊂give␈α∂rise␈α⊂to␈α⊂new␈α∂problems.␈α⊂ The␈α⊂computation␈α∂of␈α⊂a␈α⊂recursively␈α∂defined
␈↓ α∧␈↓predicate␈αmay␈αnot␈αterminate,␈αso␈αthe␈αsame␈α
problem␈αarises.␈α However,␈αwe␈αcan't␈αsolve␈αit␈αin␈α
the␈αsame
␈↓ α∧␈↓way␈αwithout␈αadding␈α
an␈αadditional␈αundefined␈α
truth␈αvalue␈αto␈α
the␈αlogic.␈α This␈α
would␈αgive␈αrise␈α
to␈αa
␈↓ α∧␈↓partial␈α⊂first␈α∂order␈α⊂logic␈α∂in␈α⊂which␈α⊂sentences␈α∂could␈α⊂be␈α∂true,␈α⊂false␈α∂or␈α⊂undefined.␈α⊂ Various␈α∂partial
␈↓ α∧␈↓predicate␈αcalculi␈αhave␈αbeen␈αstudied␈αin␈α(McCarthy␈α1964),␈α(Bochvar␈α1938␈αand␈α1943)␈αand␈αelsewhere,
␈↓ ↓H␈↓␈↓ 98
␈↓ ↓H␈↓but␈α∞they␈α∞have␈α∞the␈α∞serious␈α∞disadvantage␈α∂that␈α∞arguments␈α∞by␈α∞cases␈α∞become␈α∞quite␈α∞long,␈α∂since␈α∞three
␈↓ ↓H␈↓cases␈α∞always␈α
have␈α∞to␈α∞be␈α
provided␈α∞for,␈α∞even␈α
when␈α∞most␈α∞of␈α
the␈α∞predicates␈α∞are␈α
known␈α∞to␈α∞be␈α
total.
␈↓ ↓H␈↓Moreover,␈αexisting␈αlogic␈αtexts,␈αproof-checkers␈αand␈αtheorem␈αprovers␈αall␈αuse␈αtotal␈αlogic.␈α Therefore,
␈↓ ↓H␈↓it seems better to keep the logic conventional and handle partial predicates as functions.
␈↓ ↓H␈↓␈↓ α_We␈αintroduce␈αa␈αdomain␈α␈↓ P␈↓␈αwith␈αthree␈αelements␈α␈↓↓T,␈↓␈α␈↓↓F␈↓␈αand␈α␈↓πT␈↓␈αcalled␈αthe␈αdomain␈αof␈αextended
␈↓ ↓H␈↓truth␈α
values.␈α
In␈α
a␈α
sorted␈α
logic,␈α
this␈α
may␈α
be␈α
a␈α
separate␈α
sort.␈α
Otherwise,␈α
it␈α
may␈α
be␈αconsidered␈α
either
␈↓ ↓H␈↓separately␈α∞or␈α
as␈α∞part␈α∞of␈α
the␈α∞main␈α∞data␈α
domain.␈α∞ In␈α
Lisp␈α∞it␈α∞is␈α
convenient␈α∞to␈α∞regard␈α
␈↓↓T␈↓␈α∞and␈α∞␈↓↓F␈↓␈α
as
␈↓ ↓H␈↓special␈α
atoms␈α
and␈α
to␈α
use␈α
the␈α
same␈α
␈↓πT␈↓␈α
for␈α
extended␈α
truth␈α
values␈α
as␈α
for␈α
extended␈α
S-expressions.␈α It␈α
is
␈↓ ↓H␈↓even␈α
possible␈α∞to␈α
follow␈α
the␈α∞Lisp␈α
implementations␈α∞that␈α
use␈α
NIL␈α∞for␈α
␈↓↓F␈↓␈α
and␈α∞interpret␈α
all␈α∞other␈α
S-
␈↓ ↓H␈↓expressions as ␈↓↓T,␈↓ although we don't do that in this paper.
␈↓ ↓H␈↓␈↓ α_It␈α
is␈αconvenient␈α
to␈αdefine␈α
first␈α
a␈αform␈α
of␈αconditional␈α
expression␈α
that␈αtakes␈α
an␈αextended␈α
truth
␈↓ ↓H␈↓value as its first argument, namely
␈↓ ↓H␈↓␈↓ α_␈↓↓␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = IF p = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF p = T THEN a ELSE b␈↓.
␈↓ ↓H␈↓The␈α⊂only␈α⊂difference␈α⊂between␈α⊂then␈α⊂extended␈α⊂conditional␈α⊂expression␈α⊂and␈α⊂the␈α⊂logical␈α⊂conditional
␈↓ ↓H␈↓expression␈α⊂is␈α⊂that␈α⊂since␈α∂the␈α⊂extended␈α⊂conditional␈α⊂expression␈α∂takes␈α⊂an␈α⊂extended␈α⊂truth␈α⊂value␈α∂as
␈↓ ↓H␈↓propositional␈αargument,␈αwe␈αcan␈αprovide␈αfor␈αthe␈αpossibility␈αthat␈αthe␈αcomputation␈αof␈αthat␈αargument
␈↓ ↓H␈↓fails␈αto␈αterminate.␈α Since␈αthe␈αextended␈αconditional␈αexpression␈αtreats␈αthe␈αundefined␈αcases␈αaccording
␈↓ ↓H␈↓to their behavior in programs, we use the same notation as previously used for programs.
␈↓ ↓H␈↓␈↓ α_Extended␈α∃boolean␈α⊗operators␈α∃are␈α∃conveniently␈α⊗defined␈α∃using␈α∃the␈α⊗extended␈α∃conditional
␈↓ ↓H␈↓expressions.␈α⊃ For␈α⊃every␈α⊃predicate␈α⊃or␈α⊃boolean␈α⊃operator,␈α⊃we␈α⊃introduce␈α⊃a␈α⊃corresponding␈α⊃function
␈↓ ↓H␈↓taking␈αextended␈αtruth␈αvalues␈αas␈αoperands␈αand␈αtaking␈αan␈αextended␈αtruth␈αvalue␈αas␈αits␈αvalue.␈α Thus
␈↓ ↓H␈↓the function ␈↓↓and,␈↓ is written with an infix and defined by
␈↓ ↓H␈↓␈↓ α_␈↓↓p and q = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ F␈↓
␈↓ ↓H␈↓The␈αfunction␈α␈↓↓and␈↓␈αis␈αdistinct␈αfrom␈αthe␈αlogical␈αoperator␈α∧␈αwhich␈αremains␈αin␈αthe␈αlogic.␈α To␈αillustrate
␈↓ ↓H␈↓this, we have the true sentence
␈↓ ↓H␈↓␈↓ α_␈↓↓((p and q) = T) ≡ (p = T) ∧ (q = T)␈↓.
␈↓ ↓H␈↓The␈αparentheses␈α
in␈αthe␈αabove␈α
can␈αbe␈α
omitted␈αwithout␈αambiguity␈α
given␈αsuitable␈α
precedence␈αrules.
␈↓ ↓H␈↓Note␈αthat␈α␈↓↓and␈↓␈αhas␈αthe␈αnon-commutative␈αproperty␈αof␈α(McCarthy␈α1963),␈αnamely␈α␈↓↓F and ␈↓πT␈↓↓ = F␈↓␈α
while
␈↓ ↓H␈↓␈↓↓␈↓πT␈↓↓ and F = ␈↓πT␈↓↓␈↓.␈α This␈αcorresponds␈α
to␈αthe␈αfact␈α
that␈αit␈αis␈α
convenient␈αto␈αcompute␈α
␈↓↓p and q␈↓␈αby␈αa␈α
program
␈↓ ↓H␈↓that␈α∞doesn't␈α∞look␈α∞at␈α∞␈↓↓q␈↓␈α∞if␈α∞␈↓↓p␈↓␈α∞is␈α∞false␈α∞but␈α∞which␈α∞doesn't␈α∞terminate␈α∞if␈α∞the␈α∞computation␈α∞of␈α∂␈↓↓p␈↓␈α∞doesn't
␈↓ ↓H␈↓terminate.␈α Symmetry␈αcould␈αbe␈αrestored␈αif␈αthe␈αcomputer␈αtime-shared␈αits␈αcomputations␈αof␈α␈↓↓p␈↓␈αand␈α␈↓↓q,␈↓
␈↓ ↓H␈↓but␈αthere␈αare␈αtoo␈αmany␈αpractical␈αdisadvantages␈αto␈αsuch␈αa␈αsystem␈αto␈αjustify␈αdoing␈αit␈αfor␈αthe␈αsake␈αof
␈↓ ↓H␈↓mathematical␈αsymmetry.␈α Algol␈α60␈αrequires␈αthat␈αboth␈α␈↓↓p␈↓␈αand␈α␈↓↓q␈↓␈αbe␈αcomputed␈αwhich␈αprecludes␈αusing
␈↓ ↓H␈↓boolean opeators as the main connectives of Lisp type recursive definitions of predicates.
␈↓ ↓H␈↓␈↓ α_Other extended boolean operators are defined by
␈↓ ↓H␈↓␈↓ α_␈↓↓p or q = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ q␈↓
␈↓ α∧␈↓␈↓ u9
␈↓ α∧␈↓and
␈↓ α∧␈↓␈↓ αT␈↓↓not p = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ F ␈↓αelse␈↓↓ T␈↓.
␈↓ α∧␈↓␈↓ αTWe also require an equality function that extends logical equality, namely
␈↓ α∧␈↓␈↓ αT␈↓↓X equal Y = IF X = ␈↓πT␈↓↓ ∨ Y = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF X = Y THEN T ELSE F␈↓.
␈↓ α∧␈↓␈↓ αTReaders␈α∞familiar␈α∞with␈α∞(Manna␈α∞1974)␈α∞should␈α∞note␈α∞that␈α∞we␈α∞write␈α∞=␈α∞where␈α∞Manna␈α∞writes␈α∞≡,
␈↓ α∧␈↓and␈α
we␈α
write␈α␈↓↓equal␈↓␈α
where␈α
Manna␈αwrites␈α
=.␈α
We␈α
have␈αchosen␈α
our␈α
notation␈αto␈α
conform␈α
to␈α
that␈αof
␈↓ α∧␈↓first order logic with equality.
␈↓ α∧␈↓␈↓ αTIn␈αfact,␈αthe␈αkey␈αto␈αsuccessful␈αrepresentation␈αof␈αrecursive␈αprograms␈αin␈αfirst␈αorder␈αlogic␈αis␈αthe
␈↓ α∧␈↓simultaneous␈α∂use␈α∞of␈α∂true␈α∞equality␈α∂in␈α∞the␈α∂logic␈α∂in␈α∞order␈α∂to␈α∞make␈α∂assertions␈α∞freely␈α∂and␈α∂the␈α∞␈↓↓equal␈↓
␈↓ α∧␈↓function␈α∪that␈α∪gives␈α∀an␈α∪undefined␈α∪result␈α∪for␈α∀undefined␈α∪arguments.␈α∪ The␈α∪latter␈α∀describes␈α∪the
␈↓ α∧␈↓behavior␈α∞of␈α∞an␈α∞equality␈α∞test␈α∞within␈α∞the␈α∞program.␈α∞ The␈α∞two␈α∞forms␈α∞of␈α∞conditional␈α∂expression␈α∞are
␈↓ α∧␈↓also essential.
␈↓ α∧␈↓␈↓ αTThe partial ordering ␈↓πa␈↓ is also useful applied to extended truth values.
␈↓ α∧␈↓␈↓ αTWe summarize this in the following set of axioms:
␈↓ α∧␈↓T1: ␈↓↓(∀p)(istv p ≡ p = T ∨ p = F)␈↓
␈↓ α∧␈↓T2: ␈↓↓(∀p)(isetv p ≡ istv p ∨ p = ␈↓πT␈↓↓)␈↓
␈↓ α∧␈↓T3: ␈↓↓T ≠ F ∧ ¬istv ␈↓πT␈↓↓␈↓
␈↓ α∧␈↓T4: ␈↓↓(∀p X Y)(isetv p ⊃
␈↓ α∧␈↓↓␈↓ β4␈↓αif␈↓↓ p ␈↓αthen␈↓↓ X ␈↓αelse␈↓↓ Y = IF p = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF p = T THEN X ELSE Y)␈↓
␈↓ α∧␈↓T5: ␈↓↓(∀p)(isetv p ⊃ not p = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ F ␈↓αelse␈↓↓ T)␈↓
␈↓ α∧␈↓T6: ␈↓↓(∀p q)(isetv p ∧ isetv q ⊃ p and q = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ F)␈↓
␈↓ α∧␈↓T7: ␈↓↓(∀p q)(isetv p ∧ isetv q ⊃ p or q = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ q)␈↓
␈↓ α∧␈↓T8: ␈↓↓(∀X Y)(X equal Y = IF X = ␈↓πT␈↓↓ ∨ Y = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF X = Y THEN T ELSE F␈↓
␈↓ α∧␈↓T9: ␈↓↓(∀p)(isetv p ∧ isetv q ⊃ (p ␈↓πa␈↓↓ q ≡ p = ␈↓πT␈↓↓ ∧ (q = T ∨ q = F)))␈↓.
␈↓ ↓H␈↓␈↓ *10
␈↓ ↓H␈↓α5. The Functional Equation of a Recursive Program - Theory.
␈↓ ↓H␈↓␈↓ α_The familiar recursive program
␈↓ ↓H␈↓18)␈↓ α8 ␈↓↓u * v ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓
␈↓ ↓H␈↓is a special case of a system of mutually recursive programs which can be written
␈↓ ↓H␈↓19)␈↓ α8␈↓ α8␈↓↓f␈↓#v1␈↓#(x␈↓#v1␈↓#,...,x␈↓#vm␈↓#l1␈↓#v␈↓#) ← ␈↓ t␈↓↓␈↓#v1␈↓#(f␈↓#v1␈↓#, ... ,f␈↓#vn␈↓#,x␈↓#v1␈↓#, ... ,x␈↓#vm␈↓#l1␈↓#v␈↓#)␈↓
␈↓ ↓H␈↓␈↓ α_␈↓ α8.
␈↓ ↓H␈↓␈↓ α_␈↓ α8.
␈↓ ↓H␈↓␈↓ α_␈↓ α8.
␈↓ ↓H␈↓␈↓ α_␈↓ α8␈↓↓f␈↓#vn␈↓#(x␈↓#v1␈↓#,...,x␈↓#vm␈↓#ln␈↓#v␈↓#) ← ␈↓ t␈↓↓␈↓#vn␈↓#(f␈↓#v1␈↓#, ... ,f␈↓#vn␈↓#,x␈↓#v1␈↓#, ... ,x␈↓#vm␈↓#ln␈↓#v␈↓#)␈↓.
␈↓ ↓H␈↓Here␈α
the␈α∞␈↓ t␈↓'s␈α
are␈α∞terms␈α
in␈α∞the␈α
individual␈α∞variables␈α
␈↓↓x␈↓#v1␈↓#␈↓,␈α∞etc.␈α
and␈α∞the␈α
function␈α∞symbols␈α
␈↓↓f␈↓#v1␈↓#, ... f␈↓#vn␈↓#␈↓.
␈↓ ↓H␈↓All␈α∩the␈α∩essential␈α∩features␈α∩of␈α∩such␈α∩mutual␈α∩recursive␈α∩definitions␈α∩arise␈α∩when␈α∩there␈α∩is␈α∪only␈α∩one
␈↓ ↓H␈↓function,␈α
but␈αphenomena␈α
arise␈α
when␈αthere␈α
are␈αtwo␈α
or␈α
more␈αarguments␈α
to␈α
the␈αfunctions␈α
that␈αdo␈α
not
␈↓ ↓H␈↓arise in the one argument case - two arguments being sufficiently general. Therefore, we write
␈↓ ↓H␈↓20)␈↓ α8 ␈↓↓f(x,y) ← ␈↓ t␈↓↓(f,x,y)␈↓,
␈↓ ↓H␈↓which may also be written
␈↓ ↓H␈↓21)␈↓ α8 ␈↓↓f(x,y) ← ␈↓ t␈↓↓[f](x,y)␈↓
␈↓ ↓H␈↓when we wish to emphasize that ␈↓ t␈↓ maps a partial function ␈↓↓f␈↓ into another partial function ␈↓↓␈↓ t␈↓↓[f]␈↓.
␈↓ ↓H␈↓␈↓ α_In␈α∂this␈α⊂paper,␈α∂we␈α∂shall␈α⊂mainly␈α∂consider␈α∂recursive␈α⊂programs␈α∂over␈α∂S-expressions,␈α⊂lists␈α∂and
␈↓ ↓H␈↓integers,␈α∞but␈α∂we␈α∞can␈α∞actually␈α∂start␈α∞with␈α∞an␈α∂arbitrary␈α∞collection␈α∞of␈α∂base␈α∞functions␈α∂and␈α∞predicates
␈↓ ↓H␈↓over␈α
a␈α∞collection␈α
of␈α∞domains␈α
and␈α
define␈α∞the␈α
functions␈α∞␈↓↓computable␈α
in␈α
terms␈α∞of␈α
the␈α∞base␈α
functions␈↓.
␈↓ ↓H␈↓This␈α∩is␈α∩discussed␈α∩in␈α∩(McCarthy␈α∩1963).␈α∩ In␈α⊃a␈α∩discussion␈α∩of␈α∩the␈α∩basic␈α∩ideas,␈α∩full␈α∩generality␈α⊃is
␈↓ ↓H␈↓superfluous,␈α
and␈α
all␈αthe␈α
interesting␈α
phenomena␈αarise␈α
with␈α
a␈αsingle␈α
domain␈α
-␈αcall␈α
it␈α
␈↓↓D,␈↓␈αextended␈α
to
␈↓ ↓H␈↓␈↓↓D␈↓#
+␈↓#␈↓ by adjoining ␈↓πT␈↓ and with characteristic predicate ␈↓↓isD.␈↓
␈↓ ↓H␈↓␈↓ α_Such␈α∞a␈α
program␈α∞or␈α
system␈α∞of␈α∞mutually␈α
recursive␈α∞programs␈α
can␈α∞be␈α
regarded␈α∞as␈α∞defining␈α
a
␈↓ ↓H␈↓partial function in several ways.
␈↓ ↓H␈↓1.␈α
It␈α
can␈α
be␈α∞compiled␈α
into␈α
a␈α
machine␈α
language␈α∞program␈α
for␈α
some␈α
computer␈α∞using␈α
call-by-value.
␈↓ ↓H␈↓The␈α
resulting␈α
program␈α
is␈α
a␈αsubroutine␈α
that␈α
calls␈α
itself␈α
recursively.␈α Before␈α
it␈α
is␈α
called,␈α
the␈αvalues␈α
of
␈↓ ↓H␈↓the␈αarguments␈α
must␈αbe␈α
computed␈αand␈α
stored␈αin␈α
suitable␈αconventional␈α
registers.␈α This␈α
includes␈αits
␈↓ ↓H␈↓calls␈αto␈αitself.␈α Most␈αLisp␈αimplementations␈αas␈αwell␈αas␈αmost␈αimplementations␈αof␈αother␈αprogramming
␈↓ ↓H␈↓languages use call-by-value.
␈↓ ↓H␈↓2.␈α
It␈α
can␈α∞be␈α
compiled␈α
into␈α∞a␈α
machine␈α
language␈α
program␈α∞for␈α
some␈α
computer␈α∞using␈α
call-by-name.
␈↓ ↓H␈↓The␈α
resulting␈α
program␈α
again␈αcalls␈α
itself␈α
recursively.␈α
It␈α
is␈αcalled␈α
by␈α
storing␈α
into␈α
suitable␈αregisters
␈↓ ↓H␈↓the␈α
location␈αof␈α
programs␈αfor␈α
computing␈α
the␈αexpressions␈α
that␈αhave␈α
been␈αwritten␈α
as␈α
its␈αarguments.
␈↓ α∧␈↓␈↓ f11
␈↓ α∧␈↓Thus␈α␈↓↓((w.z)*f(u))␈↓␈αwould␈αbe␈αcompiled␈αinto␈αprogram␈αthat␈αwould␈αgive␈αthe␈αprogram␈αfor␈α␈↓↓u*v␈↓␈αpointers
␈↓ α∧␈↓to␈α⊂program␈α⊂for␈α∂computing␈α⊂␈↓↓w.z␈↓␈α⊂and␈α∂␈↓↓f(u).␈↓␈α⊂The␈α⊂program␈α∂for␈α⊂*␈α⊂could␈α∂call␈α⊂these␈α⊂other␈α∂programs
␈↓ α∧␈↓whenever␈α∪it␈α∩wanted␈α∪its␈α∪arguments.␈α∩ In␈α∪the␈α∩case␈α∪of␈α∪␈↓↓u*v,␈↓␈α∩there␈α∪is␈α∩nothing␈α∪the␈α∪program␈α∩can
␈↓ α∧␈↓profitably␈α⊂do␈α∂except␈α⊂call␈α⊂for␈α∂both␈α⊂of␈α⊂its␈α∂arguments.␈α⊂ However,␈α⊂a␈α∂program␈α⊂for␈α⊂multiplying␈α∂two
␈↓ α∧␈↓matrices␈αmight␈αcall␈αits␈αfirst␈αargument,␈αand,␈αif␈αthe␈αfirst␈αargument␈αturned␈αout␈αto␈αbe␈αthe␈αzero␈αmatrix,
␈↓ α∧␈↓not bother to call the second argument.
␈↓ α∧␈↓␈↓ αTWe␈α∀can␈α∀also␈α∀consider␈α∀evaluating␈α∀the␈α∀function␈α∀by␈α∀symbolic␈α∀computation.␈α∃ Namely,␈α∀we
␈↓ α∧␈↓substitute␈αthe␈αarguments␈αof␈αthe␈αfunction␈α*␈αfor␈α␈↓↓u␈↓␈αand␈α␈↓↓v,␈↓␈αand␈αthen␈αevaluate␈αthe␈αright␈αhand␈αside␈αof
␈↓ α∧␈↓the␈αdefinition.␈α There␈αare␈αmany␈αways␈αto␈αdo␈αthis␈αevaluation,␈αbecause␈αthere␈αmay␈αbe␈αmore␈αthan␈αone
␈↓ α∧␈↓occurrence␈α
of␈αthe␈α
function␈α
being␈αdefined␈α
on␈α
the␈αright␈α
hand␈α
side␈αof␈α
the␈α
definition,␈αbut␈α
two␈αof␈α
them
␈↓ α∧␈↓correspond to call-by-name and call-by-value respectively.
␈↓ α∧␈↓3.␈αWhen␈αevaluating␈αa␈αconditional␈αexpression,␈αalways␈αevaluate␈αthe␈αpropositional␈αterm␈αfirst␈αand␈αuse
␈↓ α∧␈↓it␈α⊃to␈α⊃decide␈α⊃which␈α⊂of␈α⊃the␈α⊃other␈α⊃terms␈α⊂to␈α⊃evaluate␈α⊃first.␈α⊃ When␈α⊂evaluating␈α⊃a␈α⊃term␈α⊃formed␈α⊂by
␈↓ α∧␈↓composition␈α
of␈α
functions,␈α
if␈α
there␈α
is␈α
only␈αone␈α
occurrence␈α
of␈α
the␈α
function␈α
being␈α
defined␈α
on␈αthe␈α
right
␈↓ α∧␈↓hand␈α∂side,␈α∂there␈α∂is␈α⊂no␈α∂choice␈α∂to␈α∂be␈α⊂made,␈α∂but␈α∂if␈α∂there␈α∂is␈α⊂more␈α∂than␈α∂one,␈α∂expand␈α⊂the␈α∂leftmost
␈↓ α∧␈↓innermost␈α∞first.␈α
If␈α∞it␈α
gives␈α∞an␈α
answer␈α∞substitute␈α∞it␈α
and␈α∞continue␈α
the␈α∞process.␈α
If␈α∞it␈α∞gives␈α
further
␈↓ α∧␈↓recursion, then proceed with its leftmost innermost, etc. This corresponds to call-by value.
␈↓ α∧␈↓4.␈αIf␈αinstead␈αof␈αexpanding␈αthe␈αleftmost␈αinnermost␈αoccurrence␈αof␈αthe␈αfunction␈αfirst,␈αwe␈αexpand␈αthe
␈↓ α∧␈↓outermost occurrences, we get an evaluation method corresponding to call-by-name.
␈↓ α∧␈↓␈↓ αTIt␈αshould␈αalso␈αbe␈αproved␈αthat␈αevaluation␈αby␈αsubstitution␈αand␈αevaluation␈αby␈αsubroutine␈αboth
␈↓ α∧␈↓using␈α∞call-by-value␈α
give␈α∞the␈α
same␈α∞results.␈α∞ The␈α
two␈α∞ways␈α
of␈α∞doing␈α
call-by-name␈α∞should␈α∞also␈α
be
␈↓ α∧␈↓proved␈α∞to␈α
give␈α∞the␈α
same␈α∞results.␈α
Such␈α∞a␈α
proof␈α∞would␈α
involve␈α∞reasoning␈α
about␈α∞the␈α∞operation␈α
of
␈↓ α∧␈↓subroutine␈α
calls␈α
and␈α
the␈α
saving␈α
of␈α
temporary␈α
storage␈α
registers␈α
on␈α
the␈α
stack.␈α
We␈α
are␈α
not␈α
aware␈αof␈α
a
␈↓ α∧␈↓published proof of these statements or even a precise statement of them.
␈↓ α∧␈↓␈↓ αTComputing␈α∀␈↓↓u*v␈↓␈α∀doesn't␈α∪show␈α∀the␈α∀difference␈α∀between␈α∪these␈α∀methods,␈α∀but␈α∀consider␈α∪the
␈↓ α∧␈↓function
␈↓ α∧␈↓22)␈↓ αt ␈↓↓morris(x,y) ← ␈↓αif␈↓↓ x equal 0 ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ morris(x - 1, morris(x, y))␈↓
␈↓ α∧␈↓introduced␈α
in␈α
(Morris␈α
1968).␈α
Evaluating␈α
␈↓↓morris(2,1)␈↓␈α
by␈α
either␈α
call-by-value␈α
method␈α
leads␈α
to␈αan
␈↓ α∧␈↓infinite␈α∞computation,␈α∞because␈α∞the␈α∞term␈α∞␈↓↓morris(x, y)␈↓␈α
has␈α∞to␈α∞be␈α∞evaluated␈α∞all␈α∞over.␈α
Call-by-name
␈↓ α∧␈↓evaluation,␈αon␈α
the␈αother␈αhand,␈α
gives␈αthe␈αanswer␈α
0,␈αbecause␈α
the␈αsecond␈αargument␈α
of␈α␈↓↓morris␈↓␈αis␈α
never
␈↓ α∧␈↓called.␈α Vuillemin␈α(1973)␈αshows␈αthat␈αwhenever␈αcall-by-value␈αgives␈αan␈αanswer,␈αcall-by-name␈αgives
␈↓ α∧␈↓the␈αsame␈αanswer,␈αbut␈αsometimes␈αcall-by-name␈αgives␈αan␈αanswer␈αwhen␈αcall-by-value␈αdoesn't.␈α If␈αwe
␈↓ α∧␈↓force␈α
a␈αprogram␈α
to␈αbe␈α
␈↓↓strict,␈↓␈α
i.e.␈α to␈α
demand␈αthat␈α
all␈α
of␈αits␈α
arguments␈αare␈α
defined,␈α
then␈αcall-by-
␈↓ α∧␈↓name and call-by-value are equi-terminating - to coin a word.
␈↓ α∧␈↓␈↓ αT(Manna 1974) also contains proofs of these assertions.
␈↓ α∧␈↓␈↓ αTExecution␈α⊗of␈α⊗recursive␈α⊗programs␈α⊗by␈α∃substitution␈α⊗is␈α⊗inefficient,␈α⊗but␈α⊗provides␈α⊗a␈α∃good
␈↓ α∧␈↓theoretical tool for classifying the more efficient subroutine methods of evaluation.
␈↓ ↓H␈↓␈↓ *12
␈↓ ↓H␈↓5.␈α
Finally,␈α
we␈αcan␈α
regard␈α
(18)␈αand␈α
(22)␈α
as␈αfunctional␈α
equations␈α
for␈α*␈α
and␈α
␈↓↓morris␈↓␈α
respectively.␈α In
␈↓ ↓H␈↓general,␈α∩a␈α∩functional␈α∩equation␈α∩may␈α∩have␈α∩many␈α∩solutions␈α∩or␈α∩none.␈α∩ However,␈α∩it␈α∩is␈α⊃essentially
␈↓ ↓H␈↓Kleene's␈α∞(1952)␈α∞first␈α∞recursion␈α∞theorem,␈α∞(see␈α∞Manna␈α∞1974,␈α∞theorem␈α∞5-2)␈α∞that␈α∞if␈α∞the␈α∞right␈α∞side␈α∞is
␈↓ ↓H␈↓␈↓↓continuous␈↓␈αin␈α
the␈αfunction␈α
being␈αdefined␈αand␈α
in␈αthe␈α
individual␈αvariables,␈αthere␈α
will␈αbe␈α
a␈αunique
␈↓ ↓H␈↓␈↓↓minimal␈↓␈α∂solution.␈α⊂ This␈α∂condition␈α∂is␈α⊂assured␈α∂if␈α⊂the␈α∂right␈α∂hand␈α⊂side␈α∂is␈α∂a␈α⊂term␈α∂built␈α⊂from␈α∂strict
␈↓ ↓H␈↓functions␈α
and␈α∞predicates␈α
by␈α∞composition␈α
and␈α∞the␈α
formation␈α∞of␈α
extended␈α∞conditional␈α
expressions.
␈↓ ↓H␈↓Continuity␈αis␈αdiscussed␈αin␈α
(Manna␈α1974).␈α It␈αis␈αnot␈α
permitted␈αto␈αuse␈αlogical␈αconditional␈α
expressions
␈↓ ↓H␈↓without␈α∃satisfying␈α∀additional␈α∃hypotheses,␈α∀and␈α∃this␈α∀restriction␈α∃prevents␈α∀true␈α∃equality␈α∃or␈α∀any
␈↓ ↓H␈↓predicate␈α
from␈αdirect␈α
use.␈α If␈α
logical␈αconditional␈α
expressions␈αwere␈α
generally␈αallowed,␈α
we␈αcould␈α
have
␈↓ ↓H␈↓sentences like
␈↓ ↓H␈↓23)␈↓ α8 ␈↓↓(∀x)(f(x) = IF f(x) = ␈↓πT␈↓↓ THEN T ELSE ␈↓πT␈↓↓)␈↓
␈↓ ↓H␈↓which␈αare␈α
self-contradictory.␈α The␈αcorresponding␈α
version␈αusing␈αextended␈α
conditional␈αexpressions,
␈↓ ↓H␈↓namely
␈↓ ↓H␈↓24)␈↓ α8 ␈↓↓(∀x)(f(x) = ␈↓αif␈↓↓ f(x) equal ␈↓πT␈↓↓ ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ ␈↓πT␈↓↓)␈↓
␈↓ ↓H␈↓is␈α∞satisfied␈α∂by␈α∞␈↓↓f(x)␈α∞=␈α∂␈↓πT␈↓↓␈↓␈α∞and␈α∞is␈α∂therefore␈α∞harmless.␈α∞ Logical␈α∂conditional␈α∞expressions␈α∞can␈α∂be␈α∞used
␈↓ ↓H␈↓when we can guarantee that the propositional part is total and in some other cases.
␈↓ ↓H␈↓␈↓ α_The␈α⊂minimal␈α⊂solution␈α⊂is␈α⊂minimal␈α⊂in␈α⊂the␈α⊃sense␈α⊂that␈α⊂any␈α⊂other␈α⊂solution␈α⊂is␈α⊂greater␈α⊃in␈α⊂the
␈↓ ↓H␈↓ordering␈αof␈αfunctions␈αpreviously␈αgiven,␈αi.e.␈αif␈α␈↓↓f␈↓␈αis␈αthe␈αminimal␈αsolution␈αand␈α␈↓ f␈↓␈αis␈αanother␈αsolution,
␈↓ ↓H␈↓then
␈↓ ↓H␈↓25)␈↓ α8 ␈↓↓(∀x y)(f(x,y) ␈↓πb␈↓↓ ␈↓ f␈↓↓(x,y))␈↓.
␈↓ ↓H␈↓␈↓ α_The␈α⊃minimal␈α⊃solution␈α⊂of␈α⊃the␈α⊃functional␈α⊂equation␈α⊃can␈α⊃therefore␈α⊂be␈α⊃characterized␈α⊃by␈α⊂the
␈↓ ↓H␈↓schema
␈↓ ↓H␈↓26)␈↓ α8 ␈↓↓(∀x y)(␈↓ f␈↓↓(x,y) = ␈↓ t␈↓↓[␈↓ f␈↓↓](x,y)) ⊃ (∀x y)(f(x,y) ␈↓πb␈↓↓ ␈↓ f␈↓↓(x,y))␈↓.
␈↓ ↓H␈↓α6. Axioms for S-expressions, Lists and Integers.
␈↓ ↓H␈↓␈↓ α_The␈αcollection␈αof␈αaxioms␈αLisp1␈αallows␈αfor␈αthe␈αpossibility␈αthat␈αthere␈αare␈αother␈αkinds␈αof␈α
entity
␈↓ ↓H␈↓besides␈αS-expressions,␈αlists␈αand␈αintegers.␈α In␈αpractical␈αprogram␈αproving,␈αthese␈αwill␈αinclude␈αsets␈αand
␈↓ ↓H␈↓data␈αstructures␈αof␈αvarious␈αkinds.␈α In␈αconsequence␈αof␈αthis␈αdecision,␈αwe␈αneed␈αthe␈α
predicates␈α␈↓↓issexp,␈↓
␈↓ ↓H␈↓␈↓↓islist␈↓␈αand␈α␈↓↓isint␈↓␈α
to␈αpick␈αout␈αS-expressions,␈α
lists␈αand␈αintegers␈αrespectively.␈α
Lists␈αare␈αconsidered␈αto␈α
be
␈↓ ↓H␈↓a␈α⊃particular␈α⊂kind␈α⊃of␈α⊃S-expression,␈α⊂namely␈α⊃S-expressions␈α⊂such␈α⊃that␈α⊃going␈α⊂in␈α⊃the␈α⊃␈↓↓cdr␈↓␈α⊂direction
␈↓ ↓H␈↓eventually␈α
reaches␈α
NIL.␈α
It␈α
is␈α
convenient␈α
to␈αhave␈α
both␈α
the␈α
predicates␈α
␈↓↓atom␈↓␈α
and␈α
␈↓↓ispair␈↓␈α
that␈αpick␈α
out
␈↓ ↓H␈↓atomic and non-atomic S-expressions respectively.
␈↓ ↓H␈↓␈↓ α_Lisp1␈α⊂is␈α⊂convenient␈α⊂for␈α⊃making␈α⊂proofs␈α⊂and␈α⊂is␈α⊃intended␈α⊂to␈α⊂treat␈α⊂S-expressions,␈α⊃lists␈α⊂and
␈↓ α∧␈↓␈↓ f13
␈↓ α∧␈↓integers␈α
as␈αsimilarly␈α
as␈α
possible.␈α Therefore,␈α
the␈α
axioms␈αare␈α
highly␈α
redundant.␈α Adjoining␈α
␈↓πT␈↓␈αto␈α
the
␈↓ α∧␈↓domains␈αhas␈αboth␈αconveniences␈αand␈αinconveniences.␈α The␈αmain␈αconvenience␈αis␈αthat␈α
the␈αrecursive
␈↓ α∧␈↓definitions␈α⊃now␈α⊃give␈α⊃total␈α⊃functions.␈α⊃ A␈α⊃major␈α⊃inconvenience␈α⊃is␈α⊃that␈α⊃algebraic␈α⊃relations␈α⊂often
␈↓ α∧␈↓require qualification, e.g. ␈↓↓0 ␈↓πx␈↓↓ x = 0␈↓ isn't true if ␈↓↓x = ␈↓πT␈↓↓␈↓.
␈↓ α∧␈↓␈↓ αTOur first axiom gives the algebraic relations of ␈↓↓cons,␈↓ ␈↓↓car␈↓ and ␈↓↓cdr.␈↓
␈↓ α∧␈↓S1: ␈↓↓(∀x y)(issexp x ∧ issexp y ⊃ ispair[x.y] ∧ ␈↓αa␈↓↓[x.y] = x ∧ ␈↓αd␈↓↓[x.y] = y)␈↓
␈↓ α∧␈↓␈↓ αTThe definition of atoms and pairs:
␈↓ α∧␈↓S2: ␈↓↓(∀x)((ispair x ≡ issexp x ∧ ¬atom x) ∧ (atom x ⊃ issexp x))␈↓
␈↓ α∧␈↓␈↓ αTTaking␈α
apart␈αan␈α
S-expression␈α
and␈αputting␈α
the␈αparts␈α
back␈α
together␈αgives␈α
back␈α
the␈αoriginal
␈↓ α∧␈↓expression.
␈↓ α∧␈↓S3: ␈↓↓(∀x)(ispair x ⊃ issexp ␈↓αa␈↓↓ x ∧ issexp ␈↓αd␈↓↓ x ∧ x = ␈↓αa␈↓↓ x . ␈↓αd␈↓↓ x)␈↓
␈↓ α∧␈↓␈↓ αTLists are included among S-expressions.
␈↓ α∧␈↓S4: ␈↓↓(∀u)(islist u ⊃ issexp u)␈↓
␈↓ α∧␈↓␈↓ αT␈↓↓cons␈↓ing an S-expression onto a list gives a list.
␈↓ α∧␈↓S5: ␈↓↓(∀x u)(issexp x ∧ islist u ⊃ islist[x.u])␈↓
␈↓ α∧␈↓␈↓ αTNIL is the only atomic list and only NIL satisfies the predicate ␈↓↓null.␈↓
␈↓ α∧␈↓S6: ␈↓↓(∀u)((islist u ∧ atom u ≡ u = ␈↓NIL␈↓↓) ∧ (null u ≡ u = ␈↓NIL␈↓↓))␈↓
␈↓ α∧␈↓␈↓ αTThe simple structural induction schema for S-expressions:
␈↓ α∧␈↓S7: ␈↓↓(∀x)(atom x ⊃ ␈↓ F␈↓↓ x) ∧ (∀x)(ispair x ∧ ␈↓ F␈↓↓ ␈↓αa␈↓↓ x ∧ ␈↓ F␈↓↓ ␈↓αd␈↓↓ x ⊃ ␈↓ F␈↓↓ x) ⊃ (∀x)(issexp x ⊃ ␈↓ F␈↓↓ x)␈↓
␈↓ α∧␈↓␈↓ αTThe simple structural induction schema for lists:
␈↓ α∧␈↓S8: ␈↓↓␈↓ F␈↓↓ ␈↓NIL␈↓↓ ∧ (∀u)(islist u ∧ ¬null u ∧ ␈↓ F␈↓↓ ␈↓αd␈↓↓ u ⊃ ␈↓ F␈↓↓ u) ⊃ (∀u)(islist u ⊃ ␈↓ F␈↓↓ u)␈↓
␈↓ α∧␈↓␈↓ αT␈↓↓x␈α
≤␈↓#vS␈↓#␈α
y␈↓␈α
means␈α
that␈α
␈↓↓x␈↓␈α
is␈α
a␈α
subexpression␈αof␈α
␈↓↓y␈↓␈α
and␈α
is␈α
a␈α
well-founded␈α
partial␈α
ordering.␈α
It␈αis
␈↓ α∧␈↓important for course-of-values induction for S-expressions.
␈↓ α∧␈↓S9: ␈↓↓(∀x y)(issexp x ∧ issexp y ⊃ x ≤␈↓#vS␈↓# y ≡ x = y ∨ ¬atom y ∧ (x ≤␈↓#vS␈↓# ␈↓αa␈↓↓ y ∨ x ≤␈↓#vS␈↓# ␈↓αd␈↓↓ y))␈↓
␈↓ α∧␈↓␈↓ αTDefinition of proper subexpression:
␈↓ α∧␈↓S10: ␈↓↓(∀x y)(x <␈↓#vS␈↓# y ≡ x ≤␈↓#vS␈↓# y ∧ x ≠ y)␈↓
␈↓ ↓H␈↓␈↓ *14
␈↓ ↓H␈↓␈↓ α_The course-of-values structural induction schema for S-expressions:
␈↓ ↓H␈↓S11: ␈↓↓(∀x)(issexp x ∧ (∀y)(issexp y ∧ y <␈↓#vS␈↓# x ⊃ ␈↓ F␈↓↓ y) ⊃ ␈↓ F␈↓↓ x) ⊃ (∀x)(issexp x ⊃ ␈↓ F␈↓↓ x)␈↓
␈↓ ↓H␈↓␈↓ α_␈↓↓u␈α≤␈↓#vL␈↓#␈αv␈↓␈αis␈αthe␈αnatural␈αwell-founded␈αpartial␈αordering␈α
for␈αlists.␈α It␈αcan␈αbe␈αread␈α"The␈αlist␈α␈↓↓u␈↓␈αis␈α
a
␈↓ ↓H␈↓tail of the list ␈↓↓v␈↓".
␈↓ ↓H␈↓S12: ␈↓↓(∀u v)(islist u ∧ islist v ⊃ u ≤␈↓#vL␈↓# v ≡ u = v ∨ ¬null v ∧ u ≤␈↓#vL␈↓# ␈↓αd␈↓↓ v)␈↓
␈↓ ↓H␈↓␈↓ α_␈↓↓u␈↓ is a proper tail of ␈↓↓v.␈↓
␈↓ ↓H␈↓S13: ␈↓↓(∀u v)(u <␈↓#vL␈↓# v ≡ u ≤␈↓#vL␈↓# v ∧ u ≠ v)␈↓
␈↓ ↓H␈↓␈↓ α_The␈αcourse-of-values␈αinduction␈αschema␈α
for␈αlists.␈α Course-of-values␈αinduction␈α
schemata␈αare
␈↓ ↓H␈↓all the same except for the ordering used.
␈↓ ↓H␈↓S14: ␈↓↓(∀u)(islist u ∧ (∀v)(islist v ∧ v <␈↓#vL␈↓# u ⊃ ␈↓ F␈↓↓ v) ⊃ ␈↓ F␈↓↓ u) ⊃ (∀u)(islist u ⊃ ␈↓ F␈↓↓ u)␈↓
␈↓ ↓H␈↓␈↓ α_These␈α∂axioms␈α∂for␈α∂integers␈α∂are␈α∂based␈α∞on␈α∂the␈α∂successor␈α∂and␈α∂predecessor␈α∂functions␈α∂and␈α∞are
␈↓ ↓H␈↓analogous␈α∞to␈α∞the␈α∞above␈α
axioms␈α∞for␈α∞S-expressions.␈α∞ They␈α∞are␈α
equivalent␈α∞to␈α∞the␈α∞usual␈α∞first␈α
order
␈↓ ↓H␈↓number theory.
␈↓ ↓H␈↓␈↓ α_The relation between the successor and predecessor functions:
␈↓ ↓H␈↓I1: ␈↓↓(∀n)(isint n ⊃ isint succ n ∧ succ n ≠ 0 ∧ pred succ n = n)␈↓
␈↓ ↓H␈↓␈↓ α_As␈α∂a␈α∂function␈α∂in␈α∂the␈α∂logic,␈α∂the␈α⊂predecessor␈α∂must␈α∂always␈α∂have␈α∂a␈α∂value.␈α∂ However␈α⊂we␈α∂say
␈↓ ↓H␈↓something about ␈↓↓pred n␈↓ only for non-zero ␈↓↓n.␈↓
␈↓ ↓H␈↓I2: ␈↓↓(∀n)(isint n ∧ n ≠ 0 ⊃ isint pred n ∧ succ pred n = n)␈↓
␈↓ ↓H␈↓␈↓ α_The simple induction schema for integers:
␈↓ ↓H␈↓I3: ␈↓↓(␈↓ F␈↓↓ 0 ∧ (∀n)(isint n ∧ n ≠ 0 ∧ ␈↓ F␈↓↓ pred n ⊃ ␈↓ F␈↓↓ n) ⊃ (∀ n)(isint n ⊃ ␈↓ F␈↓↓ n)␈↓
␈↓ ↓H␈↓␈↓ α_For course-of-values induction, we need the ordering relations.
␈↓ ↓H␈↓I4: ␈↓↓(∀m n)(isint m ∧ isint n ⊃ (m ≤ n ≡ m = n ∨ n ≠ 0 ∧ m ≤ pred n))␈↓
␈↓ ↓H␈↓␈↓ α_Proper ordering:
␈↓ ↓H␈↓I5: ␈↓↓(∀m n)(m < n ≡ m ≤ n ∧ m ≠ n)␈↓
␈↓ ↓H␈↓␈↓ α_The course-of-values schema:
␈↓ ↓H␈↓I6: ␈↓↓(∀n)(isint n ∧ (∀m)(isint m ∧ m < n ⊃ ␈↓ F␈↓↓ m) ⊃ ␈↓ F␈↓↓ n) ⊃ (∀n)(isint n ⊃ ␈↓ F␈↓↓ n)␈↓
␈↓ α∧␈↓␈↓ f15
␈↓ α∧␈↓␈↓ αTThe recursive definition of addition:
␈↓ α∧␈↓I7: ␈↓↓(∀m n)(isint m ∧ isint n ⊃ m + n = IF n = 0 THEN m ELSE succ m + pred n)␈↓
␈↓ α∧␈↓␈↓ αTMultiplication:
␈↓ α∧␈↓I8: ␈↓↓(∀m n)(isint m ∧ isint n ⊃ m ␈↓πx␈↓↓ n = IF n = 0 THEN 0 ELSE m + m ␈↓πx␈↓↓ pred n)␈↓
␈↓ α∧␈↓␈↓ αTThe␈αnext␈αgroup␈αof␈αaxioms␈αare␈αconcerned␈αwith␈αextending␈αthe␈αdomain␈αby␈αadjoining␈α␈↓πT␈↓.␈α The
␈↓ α∧␈↓predicates of the extended domains are ␈↓↓isesexp,␈↓ ␈↓↓iselist␈↓ and ␈↓↓iseint␈↓ respectively.
␈↓ α∧␈↓␈↓ αTExtending the S-expressions with ␈↓πT␈↓:
␈↓ α∧␈↓E1: ␈↓↓(∀x)(isesexp x ≡ issexp x ∨ x = ␈↓πT␈↓↓)␈↓
␈↓ α∧␈↓␈↓ αTExtending the lists with ␈↓πT␈↓:
␈↓ α∧␈↓E2: ␈↓↓(∀u)(iselist u ≡ islist u ∨ u = ␈↓πT␈↓↓)␈↓
␈↓ α∧␈↓␈↓ αTExtending the integers with ␈↓πT␈↓:
␈↓ α∧␈↓E3: ␈↓↓(∀n)(iseint n ≡ isint n ∨ n = ␈↓πT␈↓↓)␈↓
␈↓ α∧␈↓␈↓ αTWe␈α
need␈α
a␈α
function␈α
taking␈α
the␈α
value␈α∞T␈α
when␈α
its␈α
argument␈α
is␈α
an␈α
S-expression.␈α
It␈α∞will␈α
be
␈↓ α∧␈↓used in extended conditional expressions.
␈↓ α∧␈↓E4: ␈↓↓(∀x)(issexpf x = IF x = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF issexp x THEN T ELSE F)␈↓
␈↓ α∧␈↓␈↓ αTLikewise for lists:
␈↓ α∧␈↓E5: ␈↓↓(∀u)(islistf u = IF u = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF islist x THEN T ELSE F)␈↓
␈↓ α∧␈↓␈↓ αTLikewise for integers:
␈↓ α∧␈↓E6: ␈↓↓(∀n)(isintf n = IF n = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF isint x THEN T ELSE F)␈↓
␈↓ α∧␈↓␈↓ αTExtending␈αthe␈αinteger␈αfunctions␈αto␈αtake␈α␈↓πT␈↓␈αas␈αan␈αargument.␈α The␈αextension␈αis␈α␈↓↓strict,␈↓␈αi.e.␈αthe
␈↓ α∧␈↓extended values are all ␈↓πT␈↓.
␈↓ α∧␈↓E7: ␈↓↓succ ␈↓πT␈↓↓ = ␈↓πT␈↓↓ ∧ pred ␈↓πT␈↓↓ = ␈↓πT␈↓↓␈↓
␈↓ α∧␈↓␈↓ αTExtending the Lisp functions strictly to take ␈↓πT␈↓ as an argument:
␈↓ α∧␈↓E8: ␈↓↓␈↓αa␈↓↓ ␈↓πT␈↓↓ = ␈↓πT␈↓↓ ∧ ␈↓αd␈↓↓ ␈↓πT␈↓↓ = ␈↓πT␈↓↓␈↓
␈↓ α∧␈↓␈↓ αTThe strict extension of ␈↓↓cons.␈↓ (Friedman and Wise (1977) propose a non-strict extension).
␈↓ ↓H␈↓␈↓ *16
␈↓ ↓H␈↓E9: ␈↓↓(∀x)(x.␈↓πT␈↓↓ = ␈↓πT␈↓↓ ∧ ␈↓πT␈↓↓.x = ␈↓πT␈↓↓)␈↓
␈↓ ↓H␈↓␈↓ α_The functions ␈↓αa␈↓t and ␈↓αn␈↓ are defined from the predicates ␈↓↓atom␈↓ and ␈↓↓null.␈↓
␈↓ ↓H␈↓E10: ␈↓↓(∀x)(␈↓αa␈↓↓t x = IF x = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF atom x THEN T ELSE F)␈↓
␈↓ ↓H␈↓E11: ␈↓↓(∀u)(␈↓αn␈↓↓ u = IF u = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF null u THEN T ELSE F)␈↓
␈↓ ↓H␈↓α7. Forms of Induction.
␈↓ ↓H␈↓␈↓ α_All␈αproofs␈αof␈αnon-trivial␈αprogram␈αproperties␈αrequire␈αsome␈αform␈αof␈αmathematical␈αinduction.
␈↓ ↓H␈↓Methods␈α∂of␈α∂induction␈α∂can␈α∂be␈α∂divided␈α∂into␈α∂three␈α∂classes␈α∂-␈α∂induction␈α∂on␈α∂data,␈α∂various␈α⊂forms␈α∂of
␈↓ ↓H␈↓computation␈α∂induction␈α∂on␈α∂approximations␈α∂to␈α∂the␈α∂program,␈α∂and␈α∂induction␈α∂on␈α∂the␈α∂course␈α⊂of␈α∂the
␈↓ ↓H␈↓computation.␈α It␈αis␈αnot␈αcertain␈αthat␈αthat␈αthese␈αare␈αreally␈αdistinct;␈αi.e.␈α there␈αmay␈αbe␈αsystematic␈αways
␈↓ ↓H␈↓of regarding one as a form of another. In this section, we deal only with induction on data.
␈↓ ↓H␈↓␈↓ α_Induction␈αon␈αdata␈αoften␈αtakes␈αa␈αform␈αcalled␈αstructural␈αinduction␈αin␈αwhich␈αthe␈αdata␈αdomain
␈↓ ↓H␈↓consists␈α⊂of␈α⊃objects␈α⊂built␈α⊃up␈α⊂from␈α⊂elementary␈α⊃objects␈α⊂by␈α⊃a␈α⊂fixed␈α⊂finite␈α⊃set␈α⊂of␈α⊃operations.␈α⊂ The
␈↓ ↓H␈↓construction␈αof␈αS-expressions␈αfrom␈αatoms␈αby␈α␈↓↓cons␈↓␈αor␈αthe␈αconstruction␈αof␈αthe␈αintegers␈αfrom␈αzero␈αby
␈↓ ↓H␈↓the successor operation are examples.
␈↓ ↓H␈↓␈↓ α_Induction␈α∩can␈α∩take␈α∩two␈α⊃forms.␈α∩ One␈α∩form␈α∩involves␈α⊃the␈α∩constructors␈α∩or␈α∩selectors␈α∩of␈α⊃the
␈↓ ↓H␈↓domain␈α∞directly.␈α∂ Simple␈α∞list,␈α∂S-expression,␈α∞and␈α∂numerical␈α∞induction␈α∂are␈α∞examples.␈α∂ The␈α∞second
␈↓ ↓H␈↓form is a course-of-values induction schema
␈↓ ↓H␈↓27)␈↓ α8 ␈↓↓(∀x)(isD x ∧ (∀y)(isD y ∧ y < x ⊃ ␈↓ f␈↓↓ y) ⊃ ␈↓ f␈↓↓ x) ⊃ (∀x)(isD x ⊃ ␈↓ f␈↓↓ x)␈↓
␈↓ ↓H␈↓based␈α⊂on␈α⊂an␈α⊂ordering␈α⊂relation␈α⊂<␈α⊂defined␈α⊂in␈α⊂terms␈α⊂of␈α⊂the␈α⊂selector␈α⊃functions.␈α⊂ Course-of-values
␈↓ ↓H␈↓schemata␈α∂were␈α∂also␈α∂given␈α∂for␈α⊂lists,␈α∂S-expression␈α∂and␈α∂natural␈α∂numbers.␈α⊂ Course-of-values␈α∂often
␈↓ ↓H␈↓gives a proof with a simpler induction predicate than simple induction.
␈↓ ↓H␈↓A simple example is the termination of the list function ␈↓↓alt␈↓ defined by
␈↓ ↓H␈↓28)␈↓ α8 ␈↓↓alt u ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u or ␈↓αn␈↓↓ ␈↓αd␈↓↓ u ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . alt ␈↓αdd␈↓↓ u␈↓.
␈↓ ↓H␈↓Because of the ␈↓αdd␈↓, simple induction doesn't work on the obvious predicate
␈↓ ↓H␈↓29)␈↓ α8 ␈↓↓␈↓ F␈↓↓(u) ≡ islist alt u␈↓,
␈↓ ↓H␈↓but course-of-values induction does work.
␈↓ ↓H␈↓␈↓ α_In␈α∞the␈α∂simple␈α∞cases␈α∞we␈α∂have␈α∞seen␈α∂so␈α∞far,␈α∞the␈α∂induction␈α∞is␈α∂on␈α∞one␈α∞of␈α∂the␈α∞variables␈α∂in␈α∞the
␈↓ ↓H␈↓program,␈α
but␈α
this␈α
is␈α
not␈αthe␈α
general␈α
case.␈α
More␈α
generally,␈α
the␈αinduction␈α
is␈α
on␈α
some␈α
function␈αof␈α
the
␈↓ α∧␈↓␈↓ f17
␈↓ α∧␈↓variables,␈α
and␈α
the␈α
domain␈α
of␈α
this␈α
function␈α
may␈α
be␈α
quite␈α
different␈α
from␈α
that␈α
of␈α
the␈α∞variables␈α
of
␈↓ α∧␈↓the␈αprogam.␈α
Often␈αit␈α
can␈αbe␈α
taken␈αto␈α
be␈αthe␈αnatural␈α
numbers,␈αbut␈α
more␈αgenerally␈α
it␈αcan␈α
be␈αany
␈↓ α∧␈↓partially ordered domain in which all descending chains are finite.
␈↓ α∧␈↓␈↓ αTFor␈αexample␈αS-expression␈αcan␈αbe␈αreplaced␈αby␈αinduction␈αon␈αnatural␈αnumbers␈αby␈αintroducing
␈↓ α∧␈↓the function ␈↓↓size x␈↓ defined by
␈↓ α∧␈↓30)␈↓ αt ␈↓↓size x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ size ␈↓αa␈↓↓ x + size ␈↓αd␈↓↓ x␈↓
␈↓ α∧␈↓Size␈αhas␈αthe␈α
property␈αthat␈α␈↓↓size␈α␈↓αa␈↓↓␈α
x␈α<␈αsize␈αx␈↓␈α
and␈α␈↓↓size␈α␈↓αd␈↓↓␈αx␈α
<␈αsize␈αx␈↓.␈α We␈α
can␈αprove␈αthat␈α
a␈αformula
␈↓ α∧␈↓␈↓↓␈↓ F␈↓↓(x)␈↓␈αholds␈αfor␈αall␈α
S-expressions␈αby␈α"induction␈αon␈αthe␈α
size␈αof␈α␈↓↓x␈↓".␈α This␈α
is␈αdone␈αby␈αproving␈αthat␈α
the
␈↓ α∧␈↓formula ␈↓ F␈↓' given by
␈↓ α∧␈↓31)␈↓ αt ␈↓↓␈↓ F␈↓↓'(n) ≡ (∀x)(size x = n ⊃ ␈↓ F␈↓↓(x))␈↓
␈↓ α∧␈↓holds␈α⊂for␈α⊂all␈α⊂numbers␈α⊂using␈α⊂numerical␈α⊂induction.␈α⊂ In␈α⊂fact␈α⊂any␈α⊂proof␈α⊂of␈α⊂the␈α⊂formula␈α⊂␈↓ F␈↓␈α⊂by␈α∂S-
␈↓ α∧␈↓expression␈α∞induction␈α∞can␈α∞easily␈α∞be␈α∞converted␈α∞to␈α∂a␈α∞proof␈α∞of␈α∞␈↓ F␈↓'␈α∞by␈α∞numerical␈α∞induction␈α∂and␈α∞vice
␈↓ α∧␈↓versa.
␈↓ α∧␈↓␈↓ αTA␈α⊃more␈α⊃exotic␈α⊃example␈α⊂of␈α⊃this␈α⊃is␈α⊃provided␈α⊂by␈α⊃the␈α⊃Takeuchi␈α⊃function␈α⊃(Takeuchi␈α⊂1978)
␈↓ α∧␈↓defined by
␈↓ α∧␈↓32)␈↓ αt␈↓ β∧␈↓↓tak(m,n,p) ←
␈↓ α∧␈↓↓␈↓ β4␈↓αif␈↓↓ m lesseq n ␈↓αthen␈↓↓ n ␈↓αelse␈↓↓ tak(tak(m-1,n,p),tak(n-1,p,m),tak(p-1,m,n))␈↓.
␈↓ α∧␈↓␈↓ αTThe function is total when the arguments are integers and is equal to
␈↓ α∧␈↓33)␈↓ αt ␈↓↓tak0(m1,m2,m3) = IF m1 ≤ m2 THEN m2 ELSE IF m2 ≤ m3 THEN m3 ELSE m1␈↓.
␈↓ α∧␈↓The most convenient proof that ␈↓↓tak␈↓ is total uses the course-of-values schema for integers with
␈↓ α∧␈↓34)␈↓ αt ␈↓↓␈↓ F␈↓↓(n) ≡ (∀m1 m2 m3)(rank(m1,m2,m3) = n ⊃ tak(m1,m2,m3) = tak0(m1,m2,m3))␈↓,
␈↓ α∧␈↓where
␈↓ α∧␈↓35)␈↓ αt ␈↓↓rank(m1,m2,m3) = dtak1(m1-m2,m3-m2)␈↓,
␈↓ α∧␈↓and
␈↓ α∧␈↓36)␈↓ αt ␈↓↓dtak1(n1,n2) =␈↓ ∧dIF n1 ≤ 0 THEN 0
␈↓ α∧␈↓↓␈↓ ∧dELSE IF n2 ≥ 2 THEN m + n(n - 1)/2 -1
␈↓ α∧␈↓↓␈↓ ∧dELSE IF n ≥ 0 THEN m
␈↓ α∧␈↓↓␈↓ ∧dELSE IF n = -1 THEN (m + 1)(m + 2)/2 - 1
␈↓ α∧␈↓↓␈↓ ∧dELSE (m - n)(m - n + 1)/2 - m - 1␈↓.
␈↓ α∧␈↓This␈α∂is␈α∂an␈α∞example␈α∂of␈α∂the␈α∞more␈α∂general␈α∂form␈α∞of␈α∂inductive␈α∂proof.␈α∞ A␈α∂rank␈α∂function␈α∂is␈α∞defined
␈↓ α∧␈↓taking␈α∂values␈α∂in␈α∂some␈α∂inductively␈α∂ordered␈α∂domain␈α∂(in␈α∂this␈α∂case␈α∂the␈α∂natural␈α∂numbers),␈α∂and␈α∂the
␈↓ ↓H␈↓␈↓ *18
␈↓ ↓H␈↓theorem␈αis␈αproved␈αunder␈αthe␈αhypothesis␈αthat␈αit␈αis␈αtrue␈αfor␈αall␈αlower␈αrank␈αtuples␈αof␈αvariables.␈α The
␈↓ ↓H␈↓term␈α⊂␈↓↓structural␈α∂induction␈↓␈α⊂seems␈α⊂no␈α∂longer␈α⊂applicable␈α∂to␈α⊂this␈α⊂general␈α∂case,␈α⊂because␈α∂it␈α⊂is␈α⊂not␈α∂an
␈↓ ↓H␈↓induction␈α⊃on␈α⊃the␈α⊃structure␈α⊃of␈α⊃the␈α⊃data␈α⊂domain␈α⊃of␈α⊃the␈α⊃program,␈α⊃although␈α⊃it␈α⊃requires␈α⊃no␈α⊂new
␈↓ ↓H␈↓machinery␈α∂when␈α∂we␈α∞are␈α∂operating␈α∂within␈α∞first␈α∂order␈α∂logic.␈α∞ Perhaps␈α∂␈↓↓structural␈α∂induction␈↓␈α∂was␈α∞a
␈↓ ↓H␈↓misnomer␈α
anyway,␈αsince␈α
the␈α
more␈αgeneral␈α
form␈α
corresponds␈αto␈α
how␈α
mathematicians␈αalready␈α
looked
␈↓ ↓H␈↓at induction.
␈↓ ↓H␈↓␈↓ α_The␈α⊃inductively␈α⊃ordered␈α⊃set␈α⊃serving␈α⊃as␈α⊃the␈α⊃domain␈α⊃of␈α⊃the␈α⊃rank␈α⊃function␈α⊃is␈α⊃chosen␈α⊃for
␈↓ ↓H␈↓convenience,␈αwhere␈αthe␈α
object␈αis␈αto␈αget␈α
a␈αshort␈αand␈αunderstandable␈α
proof.␈α If␈αwe␈αonly␈α
care␈αabout
␈↓ ↓H␈↓whether␈αa␈αproof␈αexists␈αand␈αnot␈αhow␈αeasy␈αit␈αis␈αto␈αwrite␈αand␈αread,␈αthen␈αall␈αthe␈αdomains␈αconsidered
␈↓ ↓H␈↓so␈αfar␈αare␈αequivalent␈αto␈αthe␈αnatural␈αnumbers.␈α
To␈αget␈αsomething␈αstronger,␈αwe␈αgo␈αto␈αinduction␈α
over
␈↓ ↓H␈↓transfinite ordinal numbers - explained in most books on axiomatic set theory.
␈↓ ↓H␈↓␈↓ α_The␈α∞axiom␈α∞schema␈α∞for␈α∞induction␈α∞over␈α∞ordinals␈α∞is␈α∞just␈α∞the␈α∞usual␈α∞course-of-values␈α∞schema
␈↓ ↓H␈↓written␈α∂with␈α∂the␈α∂ordering␈α∂over␈α∂the␈α∂ordinals,␈α∂say␈α∂≤␈↓#vo␈↓#.␈α∂ In␈α∂order␈α∂to␈α∂use␈α∂it,␈α∂this␈α∂ordering␈α∂must␈α∂be
␈↓ ↓H␈↓defined,␈α
and␈α
we␈α
must␈αbe␈α
able␈α
to␈α
write␈αa␈α
rank␈α
function␈α
from␈αtuplets␈α
to␈α
ordinals.␈α
This␈αrequires␈α
that
␈↓ ↓H␈↓we␈αuse␈αa␈αnotation␈αfor␈α
ordinals,␈αand␈αany␈αgiven␈αnotation␈α
represents␈αonly␈αthe␈αordinals␈αless␈αthan␈α
some
␈↓ ↓H␈↓bound.␈α∞ Most␈α∂proofs␈α∞arising␈α∂in␈α∞practice␈α∂will␈α∞involve␈α∂only␈α∞ordinals␈α∂less␈α∞than␈α∂␈↓ w␈↓␈↓#
␈↓ ␈↓#
w␈↓␈↓#
␈↓#␈α∞which␈α∂can␈α∞be
␈↓ ↓H␈↓represented as polynomials in ␈↓ w␈↓.
␈↓ ↓H␈↓␈↓ α_An␈α⊃example␈α⊃requiring␈α⊃induction␈α⊃up␈α∩to␈α⊃␈↓ w␈↓␈↓#
2␈↓#␈α⊃is␈α⊃proving␈α⊃the␈α⊃termination␈α∩of␈α⊃Ackermann's
␈↓ ↓H␈↓function which has the functional equation
␈↓ ↓H␈↓37)␈↓ α8␈↓ α8␈↓↓(∀m n)(A(m,n) =
␈↓ ↓H␈↓↓␈↓ β(␈↓αif␈↓↓ m equal 0 ␈↓αthen␈↓↓ n+1 ␈↓αelse␈↓↓ ␈↓αif␈↓↓ n equal 0 ␈↓αthen␈↓↓ A(m-1,0) ␈↓αelse␈↓↓ A(m-1,A(m,n-1)))␈↓.
␈↓ ↓H␈↓The statement to be proved is
␈↓ ↓H␈↓38)␈↓ α8 ␈↓↓(∀α)(α < ␈↓ w␈↓↓␈↓#
2␈↓# ⊃ ␈↓ F␈↓↓(α))␈↓,
␈↓ ↓H␈↓where
␈↓ ↓H␈↓39)␈↓ α8 ␈↓↓(∀α)(␈↓ F␈↓↓(α) ≡ (∀m n)(rank(m,n) = α ⊃ isint A(m,n)))␈↓,
␈↓ ↓H␈↓and
␈↓ ↓H␈↓40)␈↓ α8␈↓↓(∀m n)(rank(m,n) = ␈↓ w␈↓↓m + n)␈↓.
␈↓ ↓H␈↓The␈α
proof␈α
is␈α
straightforward,␈αbecause␈α
␈↓↓␈↓ w␈↓↓(m-1)␈α
<␈α
␈↓ w␈↓↓m+n␈↓␈α
and␈α␈↓↓␈↓ w␈↓↓m+(n-1)␈α
<␈α
␈↓ w␈↓↓m+n␈↓,␈α
so␈α
we␈αcan␈α
assume
␈↓ ↓H␈↓␈↓↓isint␈α∞A(m-1,0)␈↓␈α∞and␈α∞␈↓↓isint␈α∞A(m,n-1)␈↓.␈α∞ From␈α∞the␈α∞latter,␈α∞it␈α∞follws␈α∞that␈α∞␈↓↓␈↓ w␈↓↓(m-1)+A(m,n-1)␈↓␈α∞<␈α∞␈↓ w␈↓m+n
␈↓ ↓H␈↓which completes the induction step.
␈↓ α∧␈↓␈↓ f19
␈↓ α∧␈↓α␈↓ αT8. An Extended Example.
␈↓ α∧␈↓␈↓ αTThe␈αSAMEFRINGE␈αproblem␈αis␈αto␈αwrite␈αa␈αprogram␈αthat␈αefficiently␈αdetermines␈αwhether␈αtwo
␈↓ α∧␈↓S-expressions␈α∞have␈α∞the␈α
same␈α∞fringe,␈α∞i.e.␈α
have␈α∞the␈α∞same␈α
atoms␈α∞in␈α∞the␈α
same␈α∞order.␈α∞ (Some␈α
people
␈↓ α∧␈↓omit␈αthe␈αNILs␈αat␈αthe␈αends␈αof␈αlists,␈αbut␈α
we␈αwill␈αtake␈αall␈αatoms).␈α Thus␈α((A.B).C)␈αand␈α(A.(B.C))␈α
have
␈↓ α∧␈↓the␈αsame␈αfringe,␈αnamely␈α(A␈αB␈αC).␈α The␈αobject␈αof␈αthe␈αoriginal␈αproblem␈αwas␈αto␈αprogram␈αit␈αusing␈αa
␈↓ α∧␈↓minimum␈α
of␈α
storage,␈αand␈α
it␈α
was␈αconjectured␈α
that␈α
co-routines␈αwere␈α
necessary␈α
to␈αdo␈α
it␈α
neatly.␈α We
␈↓ α∧␈↓shall not discuss that matter here - merely the extensional correctness of one proposed solution.
␈↓ α∧␈↓␈↓ αTThe relevant recursive definitions are
␈↓ α∧␈↓41)␈↓ αt ␈↓↓fringe x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓,
␈↓ α∧␈↓We are interested in the condition ␈↓↓fringe x = fringe y␈↓.
␈↓ α∧␈↓␈↓ αTThe function to be proved correct is ␈↓↓samefringe[x,y]␈↓ defined by the simultaneous recursion
␈↓ α∧␈↓42)␈↓ αt ␈↓↓samefringe[x, y] ← (x equal y) or [not ␈↓αa␈↓↓t x and not ␈↓αa␈↓↓t y and same[gopher x, gopher y]]␈↓,
␈↓ α∧␈↓43)␈↓ αt ␈↓↓same[x, y] ← (␈↓αa␈↓↓ x equal ␈↓αa␈↓↓ y) and samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]␈↓,
␈↓ α∧␈↓where
␈↓ α∧␈↓44)␈↓ αt ␈↓↓gopher x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ gopher ␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x]␈↓.
␈↓ α∧␈↓␈↓ αTWe need to prove that ␈↓↓samefringe␈↓ is total and
␈↓ α∧␈↓45)␈↓ αt ␈↓↓(∀xy)(samefringe[x,y] = T ≡ fringe x = fringe y)␈↓.
␈↓ α∧␈↓The functional equations are
␈↓ α∧␈↓46)␈↓ αt ␈↓↓(∀x)(fringe x = ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓),
␈↓ α∧␈↓47)␈↓ αt ␈↓↓(∀u v)(u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v])␈↓.
␈↓ α∧␈↓48)␈↓ αt␈↓ αt␈↓↓(∀x y)(samefringe[x, y] =
␈↓ α∧␈↓↓␈↓ βtx equal y or [not aat x and not aat y and same[gopher x, gopher y]])␈↓,
␈↓ α∧␈↓49)␈↓ αt ␈↓↓(∀x y)(same[x, y] = ␈↓αa␈↓↓ x equal ␈↓αa␈↓↓ y and samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]␈↓,
␈↓ α∧␈↓50)␈↓ αt ␈↓↓(∀x)(gopher x = ␈↓αif␈↓↓ ␈↓αa␈↓↓t ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ gopher ␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x])␈↓.
␈↓ α∧␈↓␈↓ αTWe␈αshall␈αnot␈α
give␈αfull␈αproofs␈αbut␈α
merely␈αthe␈αinduction␈αpredicates␈α
and␈αa␈αfew␈α
indications␈αof
␈↓ α∧␈↓the algebraic transformations. We begin with a lemma about ␈↓↓gopher␈↓.
␈↓ α∧␈↓51)␈↓ αt ␈↓↓(∀x y)(ispair gopher[x.y] ∧ atom ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓.
␈↓ ↓H␈↓␈↓ *20
␈↓ ↓H␈↓␈↓ α_This lemma can be proved by S-expression structural induction on ␈↓↓x␈↓ using the predicate
␈↓ ↓H␈↓52)␈↓ α8 ␈↓↓␈↓ F␈↓↓(x) ≡ (∀y)(ispair gopher[x.y] ∧ atom ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓.
␈↓ ↓H␈↓In␈α#the␈α#course␈α"of␈α#the␈α#proof,␈α#we␈α"use␈α#the␈α#associativity␈α"of␈α#*␈α#and␈α#the␈α"formula
␈↓ ↓H␈↓␈↓↓fringe[x.y] = fringe x * fringe y␈↓.␈α
The␈α
lemma␈α
was␈α
expressed␈α
using␈α
␈↓↓gopher[x.y]␈↓␈α
in␈α
order␈α∞to␈α
avoid
␈↓ ↓H␈↓considering␈α
atomic␈αarguments␈α
for␈α␈↓↓gopher␈↓,␈α
but␈αit␈α
could␈α
have␈αequally␈α
well␈αbe␈α
proved␈αabout␈α
␈↓↓gopher x␈↓
␈↓ ↓H␈↓with the condition ␈↓↓¬atom x␈↓.
␈↓ ↓H␈↓␈↓ α_For our proof about ␈↓↓samefringe␈↓ we need one more lemma about ␈↓↓gopher␈↓, namely
␈↓ ↓H␈↓53)␈↓ α8 ␈↓↓(∀x y)(size gopher[x.y] = size[x.y]␈↓.
␈↓ ↓H␈↓␈↓ α_This␈α∞can␈α
be␈α∞proved␈α
by␈α∞S-expression␈α
induction␈α∞on␈α∞␈↓↓x␈↓␈α
separately␈α∞or␈α
as␈α∞a␈α
part␈α∞of␈α∞the␈α
above
␈↓ ↓H␈↓lemma by including ␈↓↓size gopher[x.y] = size[x.y]␈↓ as a conjunct in (51) and (52).
␈↓ ↓H␈↓␈↓ α_The statement about ␈↓↓samefringe␈↓ is
␈↓ ↓H␈↓54)␈↓ α8 ␈↓↓(∀x y)(issexp samefringe[x,y] ∧ samefringe[x,y] = T ≡ fringe x = fringe y)␈↓,
␈↓ ↓H␈↓and it is most easily proved by induction on ␈↓↓size x + size y␈↓ using the predicate
␈↓ ↓H␈↓55)␈↓ α8␈↓ α8␈↓↓␈↓ F␈↓↓(n) ≡ (∀x y)(n = size x + size y ⊃
␈↓ ↓H␈↓↓␈↓ βxissexp samefringe[x,y] ∧ (samefringe[x,y] = T ≡ fringe x = fringe y))␈↓.
␈↓ ↓H␈↓It␈α
can␈α
also␈αbe␈α
proved␈α
using␈αthe␈α
well-foundedness␈α
of␈αlexicographic␈α
ordering␈α
of␈αthe␈α
list␈α
␈↓↓<x,␈α
␈↓αa␈↓↓␈αx>␈↓,
␈↓ ↓H␈↓but then we must decide what lexicographic orderings to include in our axiom system.
␈↓ ↓H␈↓␈↓ α_Transfinite␈α
induction␈α
is␈α∞also␈α
useful,␈α
and␈α∞can␈α
be␈α
illustrated␈α∞with␈α
a␈α
variant␈α∞␈↓↓samefringe␈↓␈α
that
␈↓ ↓H␈↓does everything in one complicated recursive definition, namely
␈↓ ↓H␈↓56)␈↓ α8␈↓ α8␈↓↓samefringe[x,y] ←
␈↓ ↓H␈↓↓␈↓ αx(x equal y) or
␈↓ ↓H␈↓↓␈↓ αxnot ␈↓αa␈↓↓t x and not ␈↓αa␈↓↓t y and
␈↓ ↓H␈↓↓␈↓ β8␈↓αif␈↓↓ ␈↓αa␈↓↓t ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ [␈↓αif␈↓↓ ␈↓αa␈↓↓t ␈↓αa␈↓↓ y ␈↓αthen␈↓↓ ␈↓αa␈↓↓ x equal ␈↓αa␈↓↓ y and samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]
␈↓ ↓H␈↓↓␈↓ ∧x␈↓αelse␈↓↓ samefringe[x, ␈↓αaa␈↓↓ y . [␈↓αda␈↓↓ y . ␈↓αd␈↓↓ y]]]
␈↓ ↓H␈↓↓␈↓ β8␈↓αelse␈↓↓ samefringe[␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x .␈↓αd␈↓↓ x], y]␈↓.
␈↓ ↓H␈↓The transfinite induction predicate then has the form
␈↓ ↓H␈↓57)␈↓ α8␈↓ α8␈↓↓␈↓ F␈↓↓(n) ≡ (∀x y)[n = ␈↓ w␈↓↓(size x + size y) + size ␈↓αa␈↓↓ x + size ␈↓αa␈↓↓ y ⊃
␈↓ ↓H␈↓↓␈↓ βxissexp samefringe[x,y] ∧ (samefringe[x,y] = T ≡ fringe x = fringe y)]␈↓.
␈↓ ↓H␈↓␈↓ α_We␈α↔would␈α↔like␈α↔to␈α↔prove␈α↔that␈α↔the␈α↔amount␈α↔of␈α↔storage␈α↔used␈α↔in␈α↔the␈α↔computation␈α⊗of
␈↓ ↓H␈↓␈↓↓samefringe[x,y]␈↓␈αaside␈α
from␈αthat␈αoccupied␈α
by␈α␈↓↓x␈↓␈α
and␈α␈↓↓y,␈↓␈αnever␈α
exceeds␈αthe␈αsum␈α
of␈αthe␈α
numbers␈αof
␈↓ ↓H␈↓␈↓↓car␈↓s␈αrequired␈αto␈αreach␈αcorresponding␈αatoms␈αin␈α␈↓↓x␈↓␈αand␈α␈↓↓y.␈↓␈αUnfortunately,␈αwe␈αcan't␈αeven␈αexpress␈αthat
␈↓ α∧␈↓␈↓ f21
␈↓ α∧␈↓fact,␈αbecause␈αwe␈α
are␈αaxiomatizing␈αthe␈αprograms␈α
as␈αfunctions,␈αand␈αthe␈α
amount␈αof␈αstorage␈αused␈α
does
␈↓ α∧␈↓not␈α∞depend␈α∞merely␈α∞on␈α∂the␈α∞function␈α∞being␈α∞computed;␈α∞it␈α∂depends␈α∞on␈α∞the␈α∞method␈α∂of␈α∞computation.
␈↓ α∧␈↓We␈αmay␈α
regard␈αsuch␈αthings␈α
as␈α␈↓↓intensional␈↓␈αproperties,␈α
but␈αany␈αcorrespondence␈α
with␈αthe␈α
notion␈αof
␈↓ α∧␈↓intensional␈α∩properties␈α∪in␈α∩intensional␈α∩logic␈α∪remains␈α∩to␈α∩be␈α∪established.␈α∩ Many␈α∪such␈α∩intensional
␈↓ α∧␈↓properties␈α∞of␈α
a␈α∞program␈α∞are␈α
extensional␈α∞properties␈α
of␈α∞certain␈α∞"derived␈α
programs",␈α∞and␈α∞some␈α
are
␈↓ α∧␈↓even extensional properties of the functional ␈↓ t␈↓.
␈↓ α∧␈↓α9. The Minimization Schema.
␈↓ α∧␈↓␈↓ αTThe␈αfunctional␈αequation␈α
of␈αa␈αprogram␈αdoesn't␈α
completely␈αcharacterize␈αit.␈α For␈α
example,␈αthe
␈↓ α∧␈↓program
␈↓ α∧␈↓58)␈↓ αt ␈↓↓f1 x ← f1 x␈↓
␈↓ α∧␈↓leads to the sentence
␈↓ α∧␈↓59)␈↓ αt ␈↓↓(∀x)(f1 x = f1 x)␈↓
␈↓ α∧␈↓which␈α
provides␈α
no␈α
information␈α
although␈αthe␈α
function␈α
␈↓↓f1␈↓␈α
is␈α
undefined␈αfor␈α
all␈α
␈↓↓x.␈↓␈α
This␈α
is␈αnot␈α
always
␈↓ α∧␈↓the case, since the program
␈↓ α∧␈↓60)␈↓ αt ␈↓↓f2 x ← (f2 x).␈↓NIL␈↓↓␈↓
␈↓ α∧␈↓has the functional equation
␈↓ α∧␈↓61)␈↓ αt ␈↓↓(∀x)(f2 x = (f2 x).␈↓NIL␈↓↓)␈↓.
␈↓ α∧␈↓from which ␈↓↓(∀x)¬issexp f2(x)␈↓ can be proved by induction.
␈↓ α∧␈↓␈↓ αTIn␈α⊃order␈α⊂to␈α⊃characterize␈α⊃recursive␈α⊂programs,␈α⊃we␈α⊃need␈α⊂some␈α⊃way␈α⊃of␈α⊂asking␈α⊃for␈α⊃the␈α⊂least
␈↓ α∧␈↓defined solution of the functional equation.
␈↓ α∧␈↓␈↓ αTSuppose the program is
␈↓ α∧␈↓62)␈↓ αt ␈↓↓f(x,y) ← ␈↓ t␈↓↓[f](x,y)␈↓
␈↓ α∧␈↓yielding the functional equation
␈↓ α∧␈↓63)␈↓ αt ␈↓↓(∀x y)(f(x,y) = ␈↓ t␈↓↓[f](x,y)␈↓.
␈↓ α∧␈↓The ␈↓↓minimization schema␈↓ is then
␈↓ α∧␈↓64)␈↓ αt ␈↓↓(∀x)(␈↓ t␈↓↓[␈↓ f␈↓↓](x) ␈↓πb␈↓↓ ␈↓ f␈↓↓(x)) ⊃ (∀x)(f(x) ␈↓πb␈↓↓ ␈↓ f␈↓↓(x))␈↓.
␈↓ α∧␈↓␈↓ αTIn the case of ␈↓↓Append␈↓ we have
␈↓ ↓H␈↓␈↓ *22
␈↓ ↓H␈↓65)␈↓ α8␈↓↓(∀u v)(␈↓ f␈↓↓(u,v) ␈↓πd␈↓↓ ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . ␈↓ f␈↓↓(␈↓αd␈↓↓ u, v)) ⊃ (∀u v)(␈↓ f␈↓↓(u,v) ␈↓πd␈↓↓ u*v)␈↓.
␈↓ ↓H␈↓␈↓ α_In␈αthe␈αschema␈α␈↓ f␈↓␈αis␈αa␈αfree␈αfunction␈αvariable␈αof␈αthe␈αappropriate␈αnumber␈αof␈αarguments.␈α The
␈↓ ↓H␈↓schema is just a translation into first order logic of Park's (1970) theorem.
␈↓ ↓H␈↓66)␈↓ α8 ␈↓↓␈↓ f␈↓↓ ␈↓πd␈↓↓ ␈↓ t␈↓↓[␈↓ f␈↓↓] ⊃ ␈↓ f␈↓↓ ␈↓πd␈↓↓ Y[␈↓ t␈↓↓]␈↓.
␈↓ ↓H␈↓Here ␈↓↓Y␈↓ is the least fixed point operator.
␈↓ ↓H␈↓[Note␈α
that␈α
this␈α
theorem␈α
is␈α
a␈α
generalization␈αto␈α
continuous␈α
functionals␈α
of␈α
the␈α
second␈α
part␈αof␈α
Kleene's
␈↓ ↓H␈↓first rescursion theorem (Kleene 1952)].
␈↓ ↓H␈↓␈↓ α_The␈α
simplest␈α
application␈α
of␈αthe␈α
schema␈α
is␈α
to␈αshow␈α
that␈α
the␈α
␈↓↓f1␈↓␈α
defined␈αby␈α
(58)␈α
is␈α
never␈αan␈α
S-
␈↓ ↓H␈↓expression. The schema becomes
␈↓ ↓H␈↓67)␈↓ α8 ␈↓↓(∀x)(␈↓ f␈↓↓ x ␈↓πd␈↓↓ ␈↓ f␈↓↓ x) ⊃ (∀x)(␈↓ f␈↓↓ x ␈↓πd␈↓↓ f1 x)␈↓,
␈↓ ↓H␈↓and we take
␈↓ ↓H␈↓68)␈↓ α8 ␈↓↓␈↓ f␈↓↓ x = ␈↓πT␈↓↓␈↓.
␈↓ ↓H␈↓The␈αleft␈αside␈αof␈α(67)␈αis␈αidentically␈αtrue,␈αand,␈αremembering␈αthat␈α␈↓πT␈↓␈αis␈αnot␈αan␈αS-expression,␈αthe␈αright
␈↓ ↓H␈↓side tells us that ␈↓↓f1 x␈↓ is never an S-expression.
␈↓ ↓H␈↓␈↓ α_The␈αminimization␈αschema␈αcan␈αsometimes␈αbe␈αused␈αto␈αshow␈αpartial␈αcorrectness.␈α For␈αexample,
␈↓ ↓H␈↓the well known 91-function is defined by the recursive program over the integers
␈↓ ↓H␈↓69)␈↓ α8 ␈↓↓f91 x ← ␈↓αif␈↓↓ x greater 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ f91 f91(x + 11)␈↓.
␈↓ ↓H␈↓The goal is to show that
␈↓ ↓H␈↓70)␈↓ α8 ␈↓↓(∀x)(f91 x = IF x > 100 THEN x - 10 ELSE 91)␈↓.
␈↓ ↓H␈↓We apply the minimization schema with
␈↓ ↓H␈↓71)␈↓ α8 ␈↓↓␈↓ f␈↓↓ x ← ␈↓αif␈↓↓ x greater 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ 91␈↓,
␈↓ ↓H␈↓and␈α
it␈αcan␈α
be␈α
shown␈αby␈α
an␈α
explicit␈αcalculation␈α
without␈α
induction␈αthat␈α
the␈α
premiss␈αof␈α
the␈αschema␈α
is
␈↓ ↓H␈↓satisfied, and this shows that ␈↓↓f91,␈↓ whenever defined has the desired value.
␈↓ ↓H␈↓␈↓ α_The␈α
method␈α
of␈α
recursion␈α
induction␈α
(McCarthy␈α1963)␈α
is␈α
also␈α
an␈α
immediate␈α
application␈αof␈α
the
␈↓ ↓H␈↓minimization␈α
schema.␈α
If␈α
we␈α
show␈α
that␈α
two␈αfunctions␈α
satisfy␈α
the␈α
schema␈α
of␈α
a␈α
recursive␈αprogram,
␈↓ ↓H␈↓we␈αshow␈αthat␈αthey␈αboth␈αequal␈αthe␈αfunction␈αcomputed␈αby␈αthe␈αprogram␈αon␈αwherever␈αthe␈αfunction␈αis
␈↓ ↓H␈↓defined.
␈↓ ↓H␈↓␈↓ α_The␈α
utility␈α
of␈α
the␈α
minimization␈αschema␈α
for␈α
proving␈α
partial␈α
correctness␈α
or␈αnon-termination
␈↓ α∧␈↓␈↓ f23
␈↓ α∧␈↓depends␈α∂on␈α∂our␈α∞ability␈α∂to␈α∂name␈α∂suitable␈α∞comparison␈α∂functions.␈α∂ f1␈α∞and␈α∂f91␈α∂were␈α∂easily␈α∞treated,
␈↓ α∧␈↓because␈α⊃the␈α⊃necessary␈α⊃comparison␈α⊃functions␈α⊃could␈α⊃be␈α⊃given␈α⊃explicitly␈α⊃without␈α⊃recursion.␈α⊂ Any
␈↓ α∧␈↓extension␈αof␈αthe␈αlanguage␈αthat␈αprovides␈αnew␈αtools␈αfor␈αnaming␈αcomparison␈αfunctions,␈αe.g.␈αgoing␈αto
␈↓ α∧␈↓higher order logic, will improve our ability to use the schema in proofs.
␈↓ α∧␈↓α10. Derived Programs and Complete Recursive Programs.
␈↓ α∧␈↓␈↓ αTThe␈αmethods␈αconsidered␈α
so␈αfar␈αin␈α
this␈αpaper␈αconcern␈α
␈↓↓extensional␈↓␈αproperties␈αof␈αprograms,␈α
i.e.
␈↓ α∧␈↓properties␈α⊗of␈α⊗the␈α∃function␈α⊗computed␈α⊗by␈α∃the␈α⊗program.␈α⊗ The␈α∃following␈α⊗are␈α⊗not␈α∃extensional
␈↓ α∧␈↓properties:␈α
the␈α
number␈α
of␈α
times␈α
a␈αcertain␈α
function␈α
is␈α
evaluated␈α
in␈α
executing␈α
the␈αprogram␈α
including
␈↓ α∧␈↓as␈α
a␈αspecial␈α
case␈α
the␈αnumber␈α
of␈αrecursions,␈α
the␈α
maximum␈αdepth␈α
of␈αrecursion,␈α
and␈α
the␈αmaximum
␈↓ α∧␈↓amount␈α∞of␈α∞storage␈α∞used.␈α∞ Some␈α∞of␈α∞these␈α∞properties␈α∞depend␈α∞on␈α∞whether␈α∞the␈α∞program␈α∞is␈α
executed
␈↓ α∧␈↓call-by-name␈α∂or␈α∂call-by-value,␈α⊂while␈α∂others␈α∂are␈α∂extensional␈α⊂properties␈α∂of␈α∂the␈α∂functional␈α⊂of␈α∂the
␈↓ α∧␈↓program.
␈↓ α∧␈↓␈↓ αTMany␈α⊂of␈α⊂these␈α⊂␈↓↓intensional␈↓␈α⊂properties␈α⊂of␈α⊂a␈α⊂program␈α⊂are␈α⊂extensional␈α⊂properties␈α⊂of␈α⊂related
␈↓ α∧␈↓programs␈αcalled␈α␈↓↓derived␈αprograms␈↓.␈α For␈αexample,␈αthe␈αnumber␈αof␈α␈↓↓cons␈↓␈αoperations␈αdone␈α
by␈α␈↓↓Append␈↓
␈↓ α∧␈↓can be computed by a program of the same recursive structure, namely
␈↓ α∧␈↓72)␈↓ αt ␈↓↓ncappend[u,v] ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ 1 + ncappend[␈↓αd␈↓↓ u, v]␈↓.
␈↓ α∧␈↓If we define ␈↓↓flat␈↓ by
␈↓ α∧␈↓73)␈↓ αt ␈↓↓flat[x,u] ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ x.u ␈↓αelse␈↓↓ flat[␈↓αa␈↓↓ x,flat[␈↓αd␈↓↓ x u]]␈↓,
␈↓ α∧␈↓then the number of recursions done by ␈↓↓flat␈↓ is given by
␈↓ α∧␈↓74)␈↓ αt ␈↓↓nrflat[x,u] ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ 1 + nrflat[␈↓αa␈↓↓ x,flat[␈↓αd␈↓↓ x,u]] + nrflat[␈↓αd␈↓↓ x,u]␈↓,
␈↓ α∧␈↓noticing␈α
that␈α␈↓↓nrflat␈↓␈α
is␈α
mutually␈αrecursive␈α
with␈α
␈↓↓flat␈↓␈αitself.␈α
The␈α
maximum␈αdepth␈α
of␈α
recursion␈αof␈α
the
␈↓ α∧␈↓91-function is given by
␈↓ α∧␈↓75)␈↓ αt ␈↓↓df91 n ← 1 + ␈↓αif␈↓↓ n greater 100 ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ max(df91(n + 11),df91(f(x + 11)))␈↓.
␈↓ α∧␈↓␈↓ αTMorris␈α
(1968)␈α
discussed␈αa␈α
derived␈α
function␈α
that␈αgives␈α
successive␈α
approximations␈αof␈α
bounded
␈↓ α∧␈↓recursion␈α
depth␈α
to␈α
a␈α
recursive␈α
function␈α
by␈α
modifying␈α
the␈α
definition␈α
to␈α
take␈α
a␈α
"rationed"␈αnumber␈α
of
␈↓ α∧␈↓allowed recursions. For ␈↓↓append␈↓ we would have
␈↓ α∧␈↓76)␈↓ αt␈↓ αt␈↓↓append1[n,u,v] ←
␈↓ α∧␈↓↓␈↓ β4␈↓αif␈↓↓ n equal 0 ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . append1[n - 1,␈↓αd␈↓↓ u,v]␈↓.
␈↓ α∧␈↓Thus␈α␈↓↓append1[n,u,v]␈↓␈αcomputes␈α␈↓↓u*v␈↓␈αbut␈αwith␈αa␈αration␈αof␈α␈↓↓n␈↓␈αrecursions.␈α If␈αthe␈αcomputation␈α
would
␈↓ α∧␈↓require more than ␈↓↓n␈↓ recursions, the value is ␈↓πT␈↓, i.e. is undefined.
␈↓ ↓H␈↓␈↓ *24
␈↓ ↓H␈↓␈↓ α_We␈α⊃can␈α∩give␈α⊃a␈α⊃general␈α∩rule␈α⊃for␈α⊃the␈α∩rationed␈α⊃recursion␈α⊃function.␈α∩ Suppose␈α⊃that␈α⊃␈↓ t␈↓␈α∩is␈α⊃a
␈↓ ↓H␈↓program for the function ␈↓↓f(x,y).␈↓
␈↓ ↓H␈↓␈↓↓P: f(x,y) ← ␈↓ t␈↓↓[f](x,y)␈↓
␈↓ ↓H␈↓Then
␈↓ ↓H␈↓␈↓↓C(P): g(n,x,y) ← ␈↓ t␈↓↓'[g](n,x,y)␈↓
␈↓ ↓H␈↓where
␈↓ ↓H␈↓77)␈↓ α8 ␈↓↓␈↓ t␈↓↓'[␈↓ f␈↓↓] = (λn x y)(␈↓αif␈↓↓ n equal 0 ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓ t␈↓↓[(λ x y)␈↓ f␈↓↓(n-1,x,y)] (x,y))␈↓
␈↓ ↓H␈↓is␈α∂a␈α∞program␈α∂for␈α∂the␈α∞rationed␈α∂recursion␈α∞function␈α∂␈↓↓g(n,x,y).␈↓␈α∂In␈α∞this␈α∂case,␈α∞the␈α∂functional␈α∂for␈α∞the
␈↓ ↓H␈↓derived␈αfunction␈αis␈αexpressed␈αby␈αa␈αformula␈αin␈αthe␈αfunctional␈αfor␈αthe␈αoriginal␈αfunction.␈α This␈αcan't
␈↓ ↓H␈↓always be done.
␈↓ ↓H␈↓␈↓ α_We␈α∞can␈α
use␈α∞the␈α∞rationed␈α
recursion␈α∞function␈α∞as␈α
an␈α∞alternate␈α∞to␈α
the␈α∞␈↓↓minimiztion␈α∞schema␈↓␈α
for
␈↓ ↓H␈↓completing the characterization of ␈↓↓f␈↓βP␈↓. Namely we have
␈↓ ↓H␈↓78)␈↓ α8 ␈↓↓(∀x y)(isD f␈↓βP␈↓(x,y) ≡ (∃n)(isD ␈↓↓f␈↓βC(P)␈↓(x,y))),
␈↓ ↓H␈↓and␈α∞whether␈α∞␈↓↓f␈↓βC(P)␈↓↓(x,y)␈↓␈α
is␈α∞defined␈α∞for␈α
given␈α∞arguments␈α∞is␈α
determined␈α∞by␈α∞its␈α∞functional␈α
equation,
␈↓ ↓H␈↓because ␈↓↓C(P)␈↓ is what (Cartwright 1978) calls a complete recursive program.
␈↓ ↓H␈↓␈↓ α_A␈α
recursive␈α
program␈α␈↓↓P␈↓␈α
is␈α
called␈αcomplete␈α
if␈α
its␈αfunctional␈α
␈↓ t␈↓␈↓βP␈↓␈α
has␈αonly␈α
one␈α
fixed␈α
point␈α␈↓↓f␈↓βP␈↓.
␈↓ ↓H␈↓Since␈αthe␈αminimization␈αschema␈αis␈αused␈αfor␈αdistinguishing␈αthe␈αleast␈αfixed␈αpoint,␈αit␈αis␈αredundant␈α
for
␈↓ ↓H␈↓complete␈α∞programs.␈α
The␈α∞idea␈α
of␈α∞complete␈α
recursive␈α∞program␈α
was␈α∞first␈α
advanced␈α∞in␈α
(Cartwright
␈↓ ↓H␈↓1978)␈α∂as␈α⊂an␈α∂alternative␈α⊂to␈α∂the␈α⊂minimization␈α∂schema␈α⊂for␈α∂completing␈α⊂the␈α∂characterization␈α⊂of␈α∂the
␈↓ ↓H␈↓function␈α⊃computed␈α⊃by␈α⊃a␈α⊃program.␈α⊃ The␈α⊃idea␈α⊃was␈α⊃to␈α⊃compute␈α⊃the␈α⊃computation␈α⊃sequence␈α⊃of␈α⊃a
␈↓ ↓H␈↓program␈α
␈↓↓P␈↓␈αwith␈α
a␈αrelated␈α
␈↓↓complete␈αrecursive␈α
program␈↓␈α␈↓↓C(P)␈↓␈α
and␈αto␈α
show␈α
metamathematically␈αthat
␈↓ ↓H␈↓for any program
␈↓ ↓H␈↓79)␈↓ α8 ␈↓↓(∀x)(f(x) = last f␈↓βC(P)␈↓↓(x)␈↓
␈↓ ↓H␈↓where␈α␈↓↓f␈↓βC(P)␈↓␈αis␈αthe␈αfunction␈αcomputed␈αby␈α␈↓↓C(P),␈↓␈αand␈α␈↓↓last␈↓␈αis␈αa␈αfunction␈αgiving␈αthe␈αlast␈αelement␈αof␈αa
␈↓ ↓H␈↓list␈α-␈α
in␈αthis␈αcase␈α
the␈αlist␈α
of␈αvalues␈αof␈α
␈↓↓f␈↓␈αarising␈α
in␈αthe␈αcomputation.␈α
Since␈αwhether␈α␈↓↓C(P)␈↓␈α
terminates
␈↓ ↓H␈↓for␈α∞given␈α∞arguments␈α∂follows␈α∞from␈α∞its␈α∞functional␈α∂equation,␈α∞(79)␈α∞allows␈α∞us␈α∂to␈α∞establish␈α∞this␈α∂for␈α∞␈↓↓P␈↓
␈↓ ↓H␈↓itself.␈α The␈αconstructions␈αof␈α(Cartwright␈α1978)␈αwere␈αsomewhat␈αinvolved␈αand␈αdiffered␈αsubstantially
␈↓ ↓H␈↓according to whether the original program was executed call-by-name or call-by-value.
␈↓ ↓H␈↓␈↓ α_The␈α∞derived␈α∞programs␈α∞that␈α∞give␈α∞the␈α∂number␈α∞of␈α∞recursions␈α∞are␈α∞complete␈α∞so␈α∞that␈α∂␈↓↓nrflat␈↓␈α∞as
␈↓ ↓H␈↓defined above satisfies
␈↓ ↓H␈↓80)␈↓ α8 ␈↓↓(∀x u)(isint nrflat[x,u] ≡ issexp flat[x,u])␈↓.
␈↓ α∧␈↓␈↓ f25
␈↓ α∧␈↓␈↓ αTA␈αprogram␈α
for␈αthe␈α
number␈αof␈α
recursions␈αdone␈α
when␈αa␈α
program␈αis␈α
evaluated␈αcall-by-name
␈↓ α∧␈↓can␈αalso␈αbe␈αgiven.␈α Thus␈αthe␈αnumber␈αof␈αrecursions␈αdone␈αin␈αevaluating␈α
␈↓↓morris[m,n]␈↓␈αcall-by-name
␈↓ α∧␈↓is given by ␈↓↓cmorris[m,0,n,0]␈↓ where
␈↓ α∧␈↓81)␈↓ αt␈↓ αt␈↓↓cmorris[m,cm,n,cn] ←
␈↓ α∧␈↓↓␈↓ β41 + cm + ␈↓αif␈↓↓ m equal 0 ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ cmorris1[m-1,0,morris[m,n],cmorris[m,0,n,cn]]␈↓.
␈↓ α∧␈↓The␈α∩idea␈α∩is␈α∪that␈α∩the␈α∩arguments␈α∩␈↓↓cm␈↓␈α∪and␈α∩␈↓↓cn␈↓␈α∩are␈α∩the␈α∪numbers␈α∩of␈α∩recursive␈α∩calls␈α∪involved␈α∩in
␈↓ α∧␈↓evaluating ␈↓↓m␈↓ and ␈↓↓n␈↓ respectively. ␈↓↓morris␈↓ and ␈↓↓cmorris␈↓ are again equi-terminating.
␈↓ α∧␈↓α11. Proof Methods as Axiom Schemata
␈↓ α∧␈↓␈↓ αTRepresenting␈α
recursive␈α
definitions␈α
in␈αfirst␈α
order␈α
logic␈α
permits␈αus␈α
to␈α
express␈α
some␈αwell␈α
known
␈↓ α∧␈↓methods for proving partial correctness as axiom schemata of first order logic.
␈↓ α∧␈↓␈↓ αTFor example, suppose we want to prove that if the input ␈↓↓x␈↓ of a function ␈↓↓f␈↓ defined by
␈↓ α∧␈↓82)␈↓ αt ␈↓↓f x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ f h x␈↓
␈↓ α∧␈↓satisfies␈α␈↓↓␈↓ F␈↓↓(x)␈↓,␈αthen␈αif␈αthe␈αfunction␈αterminates,␈αthe␈αoutput␈α␈↓↓f(x)␈↓␈αwill␈αsatisfy␈α␈↓ Y␈↓↓(x,f(x))␈↓.␈α We␈αappeal␈αto
␈↓ α∧␈↓the following ␈↓↓axiom schema of inductive assertions␈↓:
␈↓ α∧␈↓83)␈↓ αt ␈↓↓(∀x)(␈↓ F␈↓↓(x) ⊃ q(x,x)) ∧ (∀x y)(q(x,y) ⊃ ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ ␈↓ Y␈↓↓(x,y) ␈↓αelse␈↓↓ q(x,␈↓π ␈↓↓h y))
␈↓ α∧␈↓↓ ⊃ (∀x)(␈↓ F␈↓↓(x) ∧ isD f x ⊃ ␈↓ Y␈↓↓(x,f x))␈↓
␈↓ α∧␈↓where␈α␈↓↓isD␈α
f␈αx␈↓␈α
is␈αthe␈α
assertion␈αthat␈α
␈↓↓f(x)␈↓␈αis␈α
in␈αthe␈α
nominal␈αrange␈α
of␈αthe␈α
function␈αdefinition,␈α
i.e.␈αis␈α
an
␈↓ α∧␈↓integer␈α∞or␈α
an␈α∞S-expression␈α∞as␈α
the␈α∞case␈α
may␈α∞be,␈α∞and␈α
asserts␈α∞that␈α
the␈α∞computation␈α∞terminates.␈α
In
␈↓ α∧␈↓order␈α⊂to␈α⊂use␈α⊂the␈α∂schema,␈α⊂we␈α⊂must␈α⊂invent␈α∂a␈α⊂suitable␈α⊂predicate␈α⊂␈↓↓q(x,y)␈↓,␈α∂and␈α⊂this␈α⊂is␈α⊂precisely␈α∂the
␈↓ α∧␈↓method␈αof␈αinductive␈αassertions.␈α The␈αschema␈αis␈αvalid␈αfor␈αall␈αpredicates␈α␈↓ F␈↓,␈α␈↓ Y␈↓,␈αand␈α␈↓↓q␈↓,␈αand␈αa␈αsimilar
␈↓ α∧␈↓schema can be written for any collection of mutually recursive definitions that is iterative.
␈↓ α∧␈↓␈↓ αTThe␈α∂method␈α∂of␈α∞␈↓↓subgoal␈α∂induction␈↓␈α∂for␈α∞recursive␈α∂programs␈α∂was␈α∞introduced␈α∂in␈α∂(Manna␈α∞and
␈↓ α∧␈↓Pnueli␈α∂1970),␈α⊂but␈α∂they␈α∂didn't␈α⊂give␈α∂it␈α⊂a␈α∂name.␈α∂ Morris␈α⊂and␈α∂Wegbreit␈α∂(1977)␈α⊂name␈α∂it,␈α⊂extend␈α∂it
␈↓ α∧␈↓somewhat,␈α⊂and␈α⊂apply␈α⊂it␈α∂to␈α⊂Algol-like␈α⊂programs.␈α⊂ Unlike␈α∂␈↓↓inductive␈α⊂assertions␈↓,␈α⊂it␈α⊂isn't␈α⊂limited␈α∂to
␈↓ α∧␈↓iterative definitions. Thus, for the recursive program
␈↓ α∧␈↓84)␈↓ αt ␈↓↓f␈↓β5␈↓↓ x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ h x ␈↓αelse␈↓↓ g1 f␈↓β5␈↓↓ g2 x␈↓,
␈↓ α∧␈↓where ␈↓↓p␈↓ is assumed total, we have
␈↓ α∧␈↓85)␈↓ αt ␈↓↓(∀x)(p x ⊃ q(x,h x)) ∧ (∀x z)(¬p(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧ (∀x)(␈↓ F␈↓↓(x) ∧ q(x,z) ⊃ ␈↓ Y␈↓↓(x,z))
␈↓ α∧␈↓↓ ⊃ (∀x)(␈↓ F␈↓↓(x) ∧ isD(f(x)) ⊃ ␈↓ Y␈↓↓(x,f(x)))␈↓
␈↓ ↓H␈↓␈↓ *26
␈↓ ↓H␈↓␈↓ α_We␈α∞can␈α∞express␈α∞these␈α∞methods␈α∞as␈α∂axiom␈α∞schemata,␈α∞because␈α∞we␈α∞have␈α∞the␈α∞predicate␈α∂␈↓↓isD␈↓␈α∞to
␈↓ ↓H␈↓express␈α∞termination.␈α∞ The␈α∞minimization␈α∞schema␈α∞itself␈α∞can␈α∞be␈α∞proved␈α∞by␈α∞subgoal␈α∞induction.␈α
We
␈↓ ↓H␈↓need only take ␈↓↓␈↓ F␈↓↓(x) ≡ ␈↓αtrue␈↓ and ␈↓ Y␈↓↓(x,y) ≡ (y = ␈↓ f␈↓↓(x))␈↓ and ␈↓↓q(x,y) ≡ (y = ␈↓ f␈↓↓(x))␈↓.
␈↓ ↓H␈↓␈↓ α_General␈α
rules␈αfor␈α
going␈αfrom␈α
a␈αrecursive␈α
program␈α
to␈αwhat␈α
amounts␈αto␈α
the␈αsubgoal␈α
induction
␈↓ ↓H␈↓schema␈α
are␈α
given␈α
in␈α
(Manna␈α
and␈α
Pnueli␈α
1970)␈α
and␈α
(Morris␈α
and␈α
Wegbreit␈α
1977);␈α
we␈α
need␈α
only␈α
add
␈↓ ↓H␈↓a conclusion involving the ␈↓↓isD␈↓ predicate to the Manna's and Pnueli formula ␈↓↓W␈↓βP␈↓.
␈↓ ↓H␈↓␈↓ α_However,␈α∞we␈α
can␈α∞characterize␈α
subgoal␈α∞induction␈α
as␈α∞an␈α
axiom␈α∞schema.␈α
Namely,␈α∞we␈α
define
␈↓ ↓H␈↓␈↓ t␈↓↓'[q]␈↓ as an extension of ␈↓ t␈↓ mapping relations into relations. Thus if
␈↓ ↓H␈↓86)␈↓ α8 ␈↓↓␈↓ t␈↓↓[f](x) = ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ h x ␈↓αelse␈↓↓ g1 f g2 x␈↓,
␈↓ ↓H␈↓we have
␈↓ ↓H␈↓87)␈↓ α8 ␈↓↓␈↓ t␈↓↓'[q](x,y) ≡ ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ (y = h x) ␈↓αelse␈↓↓ ∃z.(q(g2 x,z) ∧ y = g1 z)␈↓.
␈↓ ↓H␈↓In general we have
␈↓ ↓H␈↓88)␈↓ α8 ␈↓↓(∀xy)(␈↓ t␈↓↓'[q](x,y) ⊃ q(x,y)) ⊃ (∀x)(isD f x ⊃ q(x,f x))␈↓,
␈↓ ↓H␈↓from␈α
which␈α
the␈α
subgoal␈α
induction␈α
rule␈α
follows␈α∞immediately␈α
given␈α
the␈α
properties␈α
of␈α
␈↓ F␈↓␈α
and␈α∞␈↓ Y␈↓.␈α
I
␈↓ ↓H␈↓am indebted to Wolfgang Polak (oral communication) for help in elucidating this relationship.
␈↓ ↓H␈↓␈↓αWARNING␈↓: The rest of this section is somewhat conjectural. There may be bugs.
␈↓ ↓H␈↓␈↓ α_The␈αextension␈α␈↓↓␈↓ t␈↓↓'[q]␈↓␈α
can␈αbe␈αdetermined␈αas␈α
follows:␈αIntroduce␈αinto␈αthe␈α
logic␈αthe␈αnotion␈α
of␈αa
␈↓ ↓H␈↓␈↓↓multi-term␈↓␈α
which␈αis␈α
formed␈αin␈α
the␈αsame␈α
way␈α
as␈αa␈α
term␈αbut␈α
allows␈αrelations␈α
written␈α
as␈αfunctions.
␈↓ ↓H␈↓For␈α∀the␈α∀present␈α∃we␈α∀won't␈α∀interpret␈α∃them␈α∀but␈α∀merely␈α∀give␈α∃rules␈α∀for␈α∀introducing␈α∃them␈α∀and
␈↓ ↓H␈↓subsequently␈α
eliminating␈αthem␈α
again␈α
to␈αget␈α
an␈α
ordinary␈αformula.␈α
Thus␈α
we␈αwill␈α
write␈α
␈↓↓q<e>␈↓␈αwhere␈α
␈↓↓e␈↓
␈↓ ↓H␈↓is␈αany␈αterm␈αor␈αmulti-term.␈α We␈αthen␈αform␈α␈↓↓␈↓ t␈↓↓'[q]␈↓␈αexactly␈αin␈αthe␈αsame␈αway␈α␈↓↓␈↓ t␈↓↓[f]␈↓␈αwas␈αformed.␈α Thus
␈↓ ↓H␈↓for the 91-function we have
␈↓ ↓H␈↓89)␈↓ α8 ␈↓↓␈↓ t␈↓↓'[q](x) = ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ x-10 ␈↓αelse␈↓↓ q<q<x+11>>␈↓.
␈↓ ↓H␈↓The␈α⊃pointy␈α⊃brackets␈α⊂indicate␈α⊃that␈α⊃we␈α⊂are␈α⊃"applying"␈α⊃a␈α⊂relation.␈α⊃ We␈α⊃now␈α⊃evaluate␈α⊂␈↓↓␈↓ t␈↓↓'[q](x,y)␈↓
␈↓ ↓H␈↓formally as follows:
␈↓ ↓H␈↓90)␈↓ α8␈↓ α8␈↓↓␈↓ t␈↓↓'[q](x,y)␈↓ ∧8≡ (␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ x-10 ␈↓αelse␈↓↓ q<q<x+11>>)(y)
␈↓ ↓H␈↓↓␈↓ ∧8≡ ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ y = x-10 ␈↓αelse␈↓↓ q(q<x+11>,y)
␈↓ ↓H␈↓↓␈↓ ∧8≡ ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ y = x-10 ␈↓αelse␈↓↓ ∃z.(q(x+11,z) ∧ q(z,y))␈↓.
␈↓ ↓H␈↓This␈α⊂last␈α⊂formula␈α∂has␈α⊂no␈α⊂pointy␈α∂brackets␈α⊂and␈α⊂is␈α∂just␈α⊂the␈α⊂formula␈α∂that␈α⊂would␈α⊂be␈α⊂obtained␈α∂by
␈↓ ↓H␈↓Manna and Pnueli or Morris and Wegbreit. The rules are as follows:
␈↓ ↓H␈↓␈↓ α_(i)␈α∂␈↓↓␈↓ t␈↓↓'[q](x)␈↓␈α∞is␈α∂just␈α∞like␈α∂␈↓↓␈↓ t␈↓↓[f](x)␈↓␈α∞except␈α∂that␈α∂␈↓↓q␈↓␈α∞replaces␈α∂␈↓↓f␈↓␈α∞and␈α∂takes␈α∞its␈α∂arguments␈α∂in␈α∞pointy
␈↓ ↓H␈↓brackets.
␈↓ α∧␈↓␈↓ f27
␈↓ α∧␈↓␈↓ αT(ii) an ordinary term ␈↓↓e␈↓ applied to ␈↓↓y␈↓ becomes ␈↓↓y = e␈↓.
␈↓ α∧␈↓␈↓ αT(iii) ␈↓↓q<e>(y)␈↓ becomes ␈↓↓q(e,y)␈↓.
␈↓ α∧␈↓␈↓ αT(iv)␈α∩␈↓↓P(q<e>)␈↓␈α∩becomes␈α⊃␈↓↓∃z.q(e,z) ∧ P(z)␈↓␈α∩when␈α∩␈↓↓P(q<e>)␈↓␈α⊃occurs␈α∩positively␈α∩in␈α∩␈↓↓␈↓ t␈↓↓'[q](x,y)␈↓␈α⊃and
␈↓ α∧␈↓becomes␈α↔␈↓↓∀z.q(e,z) ⊃ P(z)␈↓␈α↔when␈α_the␈α↔occurrence␈α↔is␈α↔negatve.␈α_ It␈α↔is␈α↔not␈α↔evident␈α_whether␈α↔an
␈↓ α∧␈↓independent semantics can be given to multi-terms.
␈↓ α∧␈↓α12. Representations Using Finite Approximations.
␈↓ α∧␈↓␈↓ αTOur␈αsecond␈αapproach␈αto␈αrepresenting␈αrecursive␈αprograms␈αby␈αfirst␈αorder␈αformulas␈αgoes␈αback
␈↓ α∧␈↓to␈α⊂G␈↓
:␈↓odel␈α⊂(1931,␈α∂1934)␈α⊂who␈α⊂showed␈α∂that␈α⊂primitive␈α⊂recursive␈α∂functions␈α⊂could␈α⊂be␈α⊂so␈α∂represented.
␈↓ α∧␈↓(Our knowledge of G␈↓
:␈↓odel's work comes from (Kleene 1952)).
␈↓ α∧␈↓␈↓ αTKleene␈α∂(1952)␈α∂calls␈α∞a␈α∂partial␈α∂function␈α∂␈↓↓f␈↓␈α∞␈↓↓representable␈↓␈α∂if␈α∂there␈α∞is␈α∂an␈α∂arithmetic␈α∂formula␈α∞␈↓↓A␈↓
␈↓ α∧␈↓with free variables ␈↓↓x␈↓ and ␈↓↓y␈↓ such that
␈↓ α∧␈↓91)␈↓ αt ␈↓↓(∀x y)((y = f(x)) ≡ A)␈↓,
␈↓ α∧␈↓where␈αan␈αarithmetic␈αformula␈αis␈αbuilt␈αup␈αfrom␈αinteger␈αconstants␈αand␈αvariables␈αusing␈αonly␈αaddition,
␈↓ α∧␈↓multiplication␈αand␈αbounded␈α
quantification.␈α Kleene␈αshowed␈αthat␈α
all␈αpartial␈αrecursive␈αfunctions␈α
are
␈↓ α∧␈↓representable.␈α The␈α
proof␈αinvolves␈αG␈↓
:␈↓odel␈α
numbering␈αpossible␈α
computation␈αsequences␈αand␈α
showing
␈↓ α∧␈↓that␈α
the␈α∞relation␈α
between␈α
sequences␈α∞and␈α
their␈α
elements␈α∞and␈α
the␈α
steps␈α∞of␈α
the␈α
computation␈α∞are␈α
all
␈↓ α∧␈↓representable.
␈↓ α∧␈↓␈↓ αTIn␈αLisp␈αless␈αmachinery␈α
is␈αneeded,␈αbecause␈αsequences␈αare␈α
Lisp␈αdata,␈αand␈αthe␈αrelation␈α
between
␈↓ α∧␈↓a␈αsequence␈α
and␈αits␈αelements␈α
is␈αgiven␈αby␈α
basic␈αLisp␈αfunctions␈α
and␈αby␈αthe␈α
␈↓↓≤␈↓#vL␈↓#␈↓␈αaxiomatized␈αin␈α
section
␈↓ α∧␈↓6 by
␈↓ α∧␈↓92)␈↓ αt ␈↓↓(∀u v)(u ≤␈↓#vL␈↓# v ≡ (u = v) ∨ ¬null v ∧ u ≤␈↓#vL␈↓# ␈↓αd␈↓↓ v)␈↓.
␈↓ α∧␈↓␈↓ αTStarting␈α∂with␈α⊂␈↓↓≤␈↓#vL␈↓#␈↓␈α∂and␈α∂the␈α⊂basic␈α∂Lisp␈α∂functions␈α⊂and␈α∂predicates␈α∂we␈α⊂will␈α∂define␈α⊂other␈α∂Lisp
␈↓ α∧␈↓predicates without recursion.
␈↓ α∧␈↓␈↓ αTFirst we define the well known Lisp function ␈↓↓assoc␈↓ whose usual recursive definition is
␈↓ α∧␈↓93)␈↓ αt ␈↓↓assoc[x,w] ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ w ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ x equal ␈↓αaa␈↓↓ w ␈↓αthen␈↓↓ ␈↓αa␈↓↓ w ␈↓αelse␈↓↓ assoc[x, ␈↓αd␈↓↓ w]␈↓
␈↓ α∧␈↓or non-recursively
␈↓ α∧␈↓94)␈↓ αt␈↓ αt␈↓↓(∀y)(y = assoc[x,w] ≡ (∀u)(u ≤␈↓#vL␈↓# w ⊃ ␈↓αaa␈↓↓ u ≠ x) ∧ y = ␈↓NIL␈↓↓
␈↓ α∧␈↓↓␈↓ ¬T∨ (∃u)(u ≤␈↓#vL␈↓# w ∧ x = ␈↓αaa␈↓↓ u ∧ y = ␈↓αa␈↓↓ u
␈↓ α∧␈↓↓␈↓ ε4∧ (∀v)(v ≤␈↓#vL␈↓# w ∧ u <␈↓#vL␈↓# v ⊃ ␈↓αaa␈↓↓ v ≠ x))␈↓
␈↓ ↓H␈↓␈↓ *28
␈↓ ↓H␈↓␈↓ α_Now suppose that
␈↓ ↓H␈↓95)␈↓ α8 ␈↓↓f x ← ␈↓ t␈↓↓[f](x)␈↓
␈↓ ↓H␈↓is␈α
a␈αrecursive␈α
program,␈αi.e.␈α
␈↓ t␈↓␈αis␈α
a␈αcontinuous␈α
functional.␈α Our␈α
non-recursive␈αdefinition␈α
of␈α
␈↓↓f␈↓␈αuses
␈↓ ↓H␈↓finite␈αapproximations␈αto␈α␈↓↓f,␈↓␈α
i.e.␈αlists␈αof␈αpairs␈α
of␈α␈↓↓(x␈↓␈α.␈αf(x)),␈αwhere␈α
each␈αpair␈αcan␈αbe␈α
computed␈αfrom
␈↓ ↓H␈↓the functional ␈↓ t␈↓ using only the pairs that follow it on the list. Thus we define
␈↓ ↓H␈↓96)␈↓ α8 ␈↓↓ok[␈↓ t␈↓↓](w) ←
␈↓ ↓H␈↓↓␈↓ αx␈↓αn␈↓↓ w or
␈↓ ↓H␈↓↓␈↓ αx␈↓αda␈↓↓ w = ␈↓ t␈↓↓[(λx)(␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc[x,␈↓αd␈↓↓ w] ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc[x,␈↓αd␈↓↓ w])](␈↓αaa␈↓↓ w) and ok[␈↓ t␈↓↓](␈↓αd␈↓↓ w)␈↓,
␈↓ ↓H␈↓or non-recursively
␈↓ ↓H␈↓97)␈↓ α8 ␈↓↓(∀w)(ok[␈↓ t␈↓↓](w) ≡
␈↓ ↓H␈↓↓␈↓ β_(∀u)(u ≤␈↓#vL␈↓# w ⊃
␈↓ ↓H␈↓↓␈↓ βX[null u ∨ ␈↓αda␈↓↓ u = ␈↓ t␈↓↓[(λx)(␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc[x,␈↓αd␈↓↓ u] ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc[x,␈↓αd␈↓↓ u])](␈↓αaa␈↓↓ u)]))␈↓
␈↓ ↓H␈↓Now we can define ␈↓↓y = f(x)␈↓ in terms of the existence of a suitable ␈↓↓w,␈↓ namely
␈↓ ↓H␈↓98)␈↓ α8 ␈↓↓(∀x y)(y = f(x) ≡
␈↓ ↓H␈↓↓␈↓ β((∃w)(ok[␈↓ t␈↓↓](w) ∧ y = ␈↓ t␈↓↓[(λx)(␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc[x,w] ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc[x,w])](x)))␈↓
␈↓ ↓H␈↓␈↓ α_It␈αmight␈αbe␈αasked␈αwhether␈α≤␈↓#vL␈↓#␈α
is␈αnecessary.␈α Couldn't␈αwe␈αrepresent␈αrecursive␈αprograms␈α
using
␈↓ ↓H␈↓just␈α⊂␈↓↓car,␈α⊃cdr,␈α⊂cons␈↓␈α⊂and␈α⊃␈↓↓atom␈↓?␈α⊂ No,␈α⊃for␈α⊂the␈α⊂following␈α⊃reason.␈α⊂ Suppose␈α⊂that␈α⊃the␈α⊂function␈α⊃␈↓↓f␈↓␈α⊂is
␈↓ ↓H␈↓representable using only the basic Lisp functions without ≤␈↓#vL␈↓#, and consider the sentence
␈↓ ↓H␈↓99)␈↓ α8 ␈↓↓(∀x)(issexp f(x))␈↓,
␈↓ ↓H␈↓asserting␈αthe␈αtotality␈α
of␈α␈↓↓f.␈↓␈αUsing␈α
the␈αrepresentation,␈αwe␈α
can␈αwrite␈α(99)␈α
as␈αa␈αsentence␈αinvolving␈α
only
␈↓ ↓H␈↓the␈α⊃basic␈α⊃Lisp␈α⊃functions␈α⊃and␈α⊃the␈α∩constant␈α⊃␈↓πT␈↓.␈α⊃ However,␈α⊃Oppen␈α⊃(1978)␈α⊃has␈α⊃shown␈α∩that␈α⊃these
␈↓ ↓H␈↓sentences are decideable, and totality isn't.
␈↓ ↓H␈↓␈↓ α_In␈α∞case␈α∞of␈α∞functions␈α∞of␈α∞several␈α∞variables,␈α∞(98)␈α∞corresponds␈α∞to␈α∞a␈α∂call-by-value␈α∞computation
␈↓ ↓H␈↓rule␈αwhile␈αthe␈αrepresentations␈αof␈αthe␈αprevious␈αsections␈αcorrespond␈αto␈αcall-by-name␈αor␈αother␈α"safe"
␈↓ ↓H␈↓rules.␈α∞ Treating␈α∞call-by-name␈α∞similarly␈α
requires␈α∞a␈α∞definition␈α∞of␈α∞␈↓↓ok␈↓␈α
in␈α∞which␈α∞some␈α∞of␈α∞the␈α
tuplets
␈↓ ↓H␈↓have some missing elements.
␈↓ ↓H␈↓Note:␈α∂Our␈α∂original␈α∂intention␈α∂was␈α∞to␈α∂take␈α∂≤␈↓#vS␈↓#␈α∂as␈α∂basic,␈α∞but␈α∂curiously,␈α∂we␈α∂have␈α∂not␈α∂succeeded␈α∞in
␈↓ ↓H␈↓defining␈α
≤␈↓#vL␈↓#␈αnon-recursively␈α
in␈α
terms␈αof␈α
≤␈↓#vS␈↓#,␈α
although␈αthe␈α
converse␈α
is␈αa␈α
consequence␈α
of␈αour␈α
general
␈↓ ↓H␈↓construction.
␈↓ α∧␈↓␈↓ f29
␈↓ α∧␈↓α13. Questions of Incompleteness.
␈↓ α∧␈↓␈↓ αTLuckham,␈αPark␈αand␈αPaterson␈α(1970)␈αhave␈αshown␈αthat␈αwhether␈αa␈αprogram␈α
schema␈αdiverges
␈↓ α∧␈↓for␈α∞every␈α∞interpretation,␈α∂whether␈α∞it␈α∞diverges␈α∞for␈α∂some␈α∞interpretation,␈α∞and␈α∞whether␈α∂two␈α∞program
␈↓ α∧␈↓schemas␈α∀are␈α∪equivalent␈α∀are␈α∀all␈α∪not␈α∀even␈α∪partially␈α∀solvable␈α∀problems.␈α∪ Manna␈α∀(1974)␈α∀has␈α∪a
␈↓ α∧␈↓thorough␈αdiscussion␈αof␈αthese␈αpoints.␈α In␈αview␈αof␈αthese␈αresults,␈αwhat␈αcan␈αbe␈αexpected␈αfrom␈αour␈αfirst
␈↓ α∧␈↓order representations?
␈↓ α∧␈↓␈↓ αTFirst␈α
let␈α
us␈α
construct␈α
a␈α
Lisp␈α
computation␈α
that␈α
does␈α
not␈α
terminate,␈α
but␈α
whose␈α
non-termination
␈↓ α∧␈↓cannot␈α
be␈α
proved␈α
from␈α
the␈αaxioms␈α
Lisp1␈α
within␈α
first␈α
order␈αlogic.␈α
We␈α
need␈α
only␈α
program␈αa␈α
proof-
␈↓ α∧␈↓checker␈α
for␈αfirst␈α
order␈α
logic,␈αset␈α
it␈α
to␈αgenerate␈α
all␈αpossible␈α
proofs␈α
starting␈αwith␈α
the␈α
axioms␈αLisp1,
␈↓ α∧␈↓and␈α
stop␈α
when␈α
it␈αfinds␈α
a␈α
proof␈α
of␈α(NIL␈α
≠␈α
NIL)␈α
or␈αsome␈α
other␈α
contradiction.␈α
Assuming␈αthe␈α
axioms
␈↓ α∧␈↓are␈α
consistent,␈αthe␈α
program␈αwill␈α
never␈α
find␈αsuch␈α
a␈αproof␈α
and␈α
will␈αnever␈α
stop.␈α In␈α
fact,␈αproving␈α
that
␈↓ α∧␈↓the␈α⊂program␈α⊂will␈α⊂never␈α⊂stop␈α⊂is␈α⊃precisely␈α⊂proving␈α⊂that␈α⊂the␈α⊂axioms␈α⊂are␈α⊂consistent.␈α⊃ But␈α⊂G␈↓
:␈↓odel's
␈↓ α∧␈↓theorem␈α⊂asserts␈α⊃that␈α⊂axiom␈α⊃systems␈α⊂like␈α⊂Lisp1␈α⊃cannot␈α⊂be␈α⊃proved␈α⊂consistent␈α⊃within␈α⊂themselves.
␈↓ α∧␈↓Until␈α∂recently,␈α⊂all␈α∂the␈α⊂known␈α∂cases␈α⊂of␈α∂sentences␈α⊂of␈α∂Peano␈α⊂arithmetic␈α∂unprovable␈α⊂within␈α∂Peano
␈↓ α∧␈↓arithmetic␈α∀involved␈α∀such␈α∀an␈α∀appeal␈α∀to␈α∀G␈↓
:␈↓odel's␈α∀theorem␈α∀or␈α∀similar␈α∀unsolvability␈α∀arguments.
␈↓ α∧␈↓However,␈α∃Paris␈α∃and␈α∃Harrington␈α∃(1977)␈α∃found␈α∃a␈α∃form␈α∃of␈α∃Ramsey's␈α∃theorem␈α⊗a␈α∃well-known
␈↓ α∧␈↓combinatorial␈α∂theorem,␈α⊂that␈α∂could␈α∂be␈α⊂proved␈α∂unprovable␈α∂in␈α⊂Peano␈α∂arithmetic.␈α⊂ However,␈α∂their
␈↓ α∧␈↓proof of its unprovability involved showing that it implied the consistency of Peano arithmetic.
␈↓ α∧␈↓␈↓ αTWe␈α
can␈α
presumably␈α
prove␈α
Lisp1␈α
consistent␈α
just␈α
as␈α
Gentzen␈α
proved␈α
arithmetic␈α∞consistent␈α
-
␈↓ α∧␈↓by␈α∩introducing␈α∪a␈α∩new␈α∩axiom␈α∪schema␈α∩that␈α∩allows␈α∪induction␈α∩up␈α∩to␈α∪the␈α∩transfinite␈α∪ordinal␈α∩ε␈↓β0␈↓.
␈↓ α∧␈↓Proving the new system consistent would require induction up to a still higher ordinal, etc.
␈↓ α∧␈↓␈↓ αTSince␈α∞every␈α∞recursively␈α∞defined␈α∞function␈α∞can␈α∞be␈α∞defined␈α∞explicitly,␈α∞any␈α∞sentence␈α
involving
␈↓ α∧␈↓such␈α
functions␈α
can␈α
be␈α
replaced␈α
by␈α
an␈α
equivalent␈α
sentence␈α
involving␈α
only␈α
␈↓↓≤␈↓#vL␈↓#␈↓␈α
and␈α
the␈α∞basic␈α
Lisp
␈↓ α∧␈↓functions.␈α
The␈α
theory␈αof␈α
␈↓↓≤␈↓#vL␈↓#␈↓␈α
and␈α
these␈αfunctions␈α
has␈α
a␈αstandard␈α
model,␈α
the␈α
usual␈αS-expressions
␈↓ α∧␈↓and␈α∪many␈α∩non-standard␈α∪models.␈α∩ We␈α∪"construct"␈α∩non-standard␈α∪models␈α∩in␈α∪the␈α∩usual␈α∪way␈α∩by
␈↓ α∧␈↓appealing␈α
to␈α
the␈α
theorem␈α
that␈α
if␈α
every␈α
finite␈α
subset␈α
of␈α
a␈α
set␈α
␈↓↓S␈↓␈α
of␈α
sentences␈α
of␈α
first␈α
order␈α
logic␈αhas␈α
a
␈↓ α∧␈↓model,␈α∞then␈α
␈↓↓S␈↓␈α∞has␈α∞a␈α
model.␈α∞ For␈α∞example,␈α
take␈α∞␈↓↓S␈α∞=␈α
{␈↓NIL␈↓↓␈α∞≤␈↓#vL␈↓#␈α
x,␈α∞␈↓(A)␈α∞␈↓↓≤␈↓#vL␈↓#␈↓␈α
x,␈α∞(A␈α∞A)␈↓↓␈α
≤␈↓#vL␈↓#␈α∞x,␈α∞,␈α
...␈↓
␈↓ α∧␈↓indefinitely}.␈α
Every␈αfinite␈α
subset␈αof␈α
␈↓↓S␈↓␈α
has␈αa␈α
model;␈αwe␈α
need␈αonly␈α
take␈α
␈↓↓x␈↓␈αto␈α
be␈αthe␈α
longest␈α
list␈αof
␈↓ α∧␈↓A's␈αoccurring␈αin␈αthe␈αsentences.␈α Hence␈αthere␈αis␈αa␈α
model␈αof␈αthe␈αLisp␈αaxioms␈αin␈αwhich␈α␈↓↓x␈↓␈αhas␈αall␈α
lists
␈↓ α∧␈↓of␈αA's␈αas␈αsubexpressions.␈α No␈αsentence␈αtrue␈αin␈αthe␈αstandard␈αmodel␈αand␈αfalse␈αin␈αsuch␈αa␈αmodel␈αcan
␈↓ α∧␈↓be␈α∪proved␈α∪from␈α∩the␈α∪axioms.␈α∪ However,␈α∪it␈α∩is␈α∪necessary␈α∪to␈α∪be␈α∩careful␈α∪about␈α∪the␈α∪meaning␈α∩of
␈↓ α∧␈↓termination␈αof␈αa␈αfunction.␈α In␈αfact,␈αtaking␈αsuccessive␈α␈↓↓cdr␈↓s␈αof␈αsuch␈αan␈α␈↓↓x␈↓␈αwould␈αnever␈αterminate,␈αbut
␈↓ α∧␈↓the␈α∂sentence␈α∂whose␈α∂␈↓↓standard␈α∂interpretation␈↓␈α∂is␈α∂termination␈α∂of␈α∂the␈α∂computation␈α∂is␈α∂provable␈α∞from
␈↓ α∧␈↓Lisp1.
␈↓ α∧␈↓␈↓ αTThe␈α⊂practical␈α⊂question␈α∂is:␈α⊂where␈α⊂does␈α∂the␈α⊂correctness␈α⊂of␈α∂ordinary␈α⊂programs␈α⊂come␈α⊂in?␈α∂ It
␈↓ α∧␈↓seems␈αlikely␈α
that␈αsuch␈α
statements␈αwill␈αbe␈α
provable␈αwith␈α
our␈αoriginal␈αsystem␈α
of␈αaxioms.␈α
It␈αdoesn't
␈↓ α∧␈↓follow␈α
that␈α
the␈α
system␈α
Lisp1␈α
will␈α∞permit␈α
convenient␈α
proofs,␈α
but␈α
probably␈α
it␈α
will.␈α∞ Some␈α
heuristic
␈↓ α∧␈↓evidence␈α
for␈α
this␈α
comes␈α
from␈α
(Cohen␈α
1965).␈α
Cohen␈α
presents␈α
two␈α
systems␈α
of␈α
axiomatized␈α
arithmetic
␈↓ α∧␈↓Z1␈α
and␈α
Z2.␈α
Z1␈α∞is␈α
ordinary␈α
Peano␈α
arithmetic␈α∞with␈α
an␈α
axiom␈α
schema␈α∞of␈α
induction,␈α
and␈α
Z2␈α∞is␈α
an
␈↓ α∧␈↓axiomatization␈α
of␈αhereditarily␈α
finite␈α
sets␈αof␈α
integers.␈α Superficially,␈α
Z2␈α
is␈αmore␈α
powerful␈α
than␈αZ1,
␈↓ α∧␈↓but␈αbecause␈αthe␈αset␈αoperations␈αof␈αZ2␈αcan␈αbe␈αrepresented␈αin␈αZ1␈αas␈αfunctions␈αon␈αthe␈αG␈↓
:␈↓odel␈αnumbers
␈↓ ↓H␈↓␈↓ *30
␈↓ ↓H␈↓of␈α⊃the␈α⊃sets,␈α∩it␈α⊃turns␈α⊃out␈α∩that␈α⊃Z1␈α⊃is␈α⊃just␈α∩as␈α⊃powerful␈α⊃once␈α∩the␈α⊃necessary␈α⊃machinery␈α∩has␈α⊃been
␈↓ ↓H␈↓established.␈α Because␈αsets␈αand␈αlists␈αare␈αthe␈αbasic␈αdata␈αof␈αLisp1,␈αand␈αsets␈αare␈αeasily␈αrepresented,␈αthe
␈↓ ↓H␈↓power␈αof␈αLisp1␈αwill␈αbe␈αapproximately␈αthat␈αof␈αZ2,␈αand␈αconvenient␈αproofs␈αof␈αcorrectness␈αstatements
␈↓ ↓H␈↓should␈α
be␈αpossible.␈α
Moreover,␈α
since␈αLisp1␈α
is␈αa␈α
first␈α
order␈αtheory,␈α
it␈α
is␈αeasily␈α
extended␈αwith␈α
axioms
␈↓ ↓H␈↓for sets, and this should help make informal proofs easy to express.
␈↓ ↓H␈↓␈↓ε A␈α
PUB␈α
source␈α
of␈α
this␈α
paper␈α
is␈α
available␈α
on␈α
disk␈α
at␈α
the␈α
Stanford␈α
Artificial␈α
Intelligence␈αLaboratory␈α
with
␈↓ ↓H␈↓εthe file name FIRST[W79,JMC].␈↓
␈↓ ↓H␈↓α14. References.
␈↓ ↓H␈↓␈↓αBochvar,␈α∞D.A.␈α∂(1938)␈↓:␈α∞"On␈α∂a␈α∞three-valued␈α∂logical␈α∞calculus␈α∞and␈α∂its␈α∞application␈α∂to␈α∞the␈α∂analysis␈α∞of
␈↓ ↓H␈↓contradictions", ␈↓↓Recueil Mathematique␈↓, N.S. 4 pp. 287-308.
␈↓ ↓H␈↓␈↓αBochvar,␈α≠D.A.␈α≠(1943)␈↓:␈α≠"On␈α≠the␈α~consistency␈α≠of␈α≠a␈α≠three-valued␈α≠logical␈α≠calculus",␈α~␈↓↓Recueil
␈↓ ↓H␈↓↓Mathematique␈↓, N.S. 12, pp. 353-369.
␈↓ ↓H␈↓The above Russian language papers by Bochvar are available in English translation as
␈↓ ↓H␈↓␈↓αBochvar,␈α⊂D.A.␈α⊂(1972)␈↓:␈α⊂␈↓↓Two␈α⊂papers␈α⊂on␈α⊂partial␈α⊂predicate␈α⊂calculus␈↓,␈α⊂Stanford␈α⊂Artificial␈α⊂Intelligence
␈↓ ↓H␈↓Memo␈α∪165,␈α∪Computer␈α∪Science␈α∪Department,␈α∪Stanford␈α∪University,␈α∪Stanford,␈α∪CA␈α∀94305.␈α∪ (Also
␈↓ ↓H␈↓available from NTIS).
␈↓ ↓H␈↓␈↓αCartwright,␈αR.S.␈α(1976)␈↓:␈α
␈↓↓A␈αPractical␈αFormal␈α
Semantic␈αDefinition␈αand␈α
Verification␈αSystem␈αfor␈α
Typed
␈↓ ↓H␈↓↓Lisp␈↓, Ph.D. Thesis, Computer Science Department, Stanford University, Stanford, California.
␈↓ ↓H␈↓␈↓αCartwright,␈α∩R.␈α∩(1978)␈↓:␈α∪␈↓↓First␈α∩Order␈α∩Semantics:␈α∩A␈α∪Natural␈α∩Programming␈α∩Logic␈α∪for␈α∩Recursively
␈↓ ↓H␈↓↓Defined␈α∂Functions␈↓,␈α⊂Cornell␈α∂University␈α∂Computer␈α⊂Science␈α∂Department␈α∂Technical␈α⊂Report␈α∂TR78-
␈↓ ↓H␈↓339, Ithaca, New York.
␈↓ ↓H␈↓␈↓αCartwright,␈α⊗Robert␈α⊗and␈α⊗John␈α⊗McCarthy␈α⊗(1979)␈↓:␈α⊗"First␈α⊗Order␈α⊗Programming␈α↔Logic",␈α⊗paper
␈↓ ↓H␈↓presented␈α∀at␈α∪the␈α∀sixth␈α∀annual␈α∪ACM␈α∀Symposium␈α∀on␈α∪Principles␈α∀of␈α∀Programming␈α∪Languages
␈↓ ↓H␈↓(POPL), San Antonio, Texas. Available from ACM.
␈↓ ↓H␈↓␈↓αCohen, Paul (1966)␈↓: ␈↓↓Set Theory and the Continuum Hypothesis␈↓, W.A. Benjamin Inc.
␈↓ ↓H␈↓␈↓αCooper,␈αD.C.␈α(1969)␈↓:␈α"Program␈αScheme␈αEquivalences␈αand␈αSecond-order␈αLogic",␈αin␈αB.␈αMeltzer␈αand
␈↓ ↓H␈↓D. Michie (eds.), ␈↓↓Machine Intelligence␈↓, Vol. 4, pp. 3-15, Edinburgh University Press, Edinburgh.
␈↓ ↓H␈↓␈↓αFriedman,␈αDaniel␈αand␈αDavid␈αWise(1976)␈↓:␈α"Cons␈α
should␈αnot␈αEvaluate␈αIts␈αArguments",␈αin␈α␈↓↓Proc.␈α
3rd
␈↓ ↓H␈↓↓Intl. Colloq. on Automata, Languages and Programming␈↓, Edinburgh Univ. Press, Edinburgh.
␈↓ ↓H␈↓␈↓αHitchcock,␈α
P.␈α
and␈α
D.␈α
Park␈α
(1973)␈↓:␈α
"Induction␈α
Rules␈α
and␈α
Proofs␈α
of␈α
Program␈α
Termination,␈α∞in␈α
M.
␈↓ ↓H␈↓Nivat (ed.), ␈↓↓Automata, Languages and Programming␈↓, pp. 225-251, North-Holland, Amsterdam.
␈↓ ↓H␈↓␈↓αKleene, S.C. (1952)␈↓: ␈↓↓Introduction to Metamathematics␈↓, Van Nostrand, New York.
␈↓ α∧␈↓␈↓ f31
␈↓ α∧␈↓␈↓αLuckham,␈αD.C.,␈αD.M.R.Park,␈α
and␈αM.S.␈αPaterson␈α(1970)␈↓:␈α
"On␈αFormalized␈αComputer␈αPrograms",␈α
␈↓↓J.
␈↓ α∧␈↓↓CSS␈↓, ␈↓α4␈↓(3): 220-249 (June).
␈↓ α∧␈↓␈↓αManna,␈αZohar␈αand␈α
Amir␈αPnueli␈α(1970)␈↓:␈α
"Formalization␈αof␈αthe␈α
Properties␈αof␈αFunctional␈α
Programs",
␈↓ α∧␈↓␈↓↓J. ACM␈↓, ␈↓α17␈↓(3): 555-569.
␈↓ α∧␈↓␈↓αManna, Zohar (1974)␈↓: ␈↓↓Mathematical Theory of Computation␈↓, McGraw-Hill.
␈↓ α∧␈↓␈↓αManna,␈α∀Zohar,␈α∀Stephen␈α∀Ness␈α∀and␈α∀Jean␈α∀Vuillemin␈α∀(1973)␈↓:␈α∀"Inductive␈α∀Methods␈α∀for␈α∀Proving
␈↓ α∧␈↓Properties of Programs", ␈↓↓Comm. ACM␈↓,␈↓α16␈↓(8): 491-502 (August).
␈↓ α∧␈↓␈↓αMcCarthy,␈αJohn␈α(1963)␈↓:␈α"A␈αBasis␈αfor␈αa␈α
Mathematical␈αTheory␈αof␈αComputation",␈αin␈αP.␈αBraffort␈α
and
␈↓ α∧␈↓D.␈α⊃Hirschberg␈α⊃(eds.),␈α⊂␈↓↓Computer␈α⊃Programming␈α⊃and␈α⊂Formal␈α⊃Systems␈↓,␈α⊃pp.␈α⊃33-70.␈α⊂ North-Holland
␈↓ α∧␈↓Publishing Company, Amsterdam.
␈↓ α∧␈↓␈↓αMcCarthy,␈αJohn␈α(1964)␈↓:␈α␈↓↓Predicate␈αCalculus␈αwith␈α"Undefined"␈αas␈αa␈αTruth␈αValue␈↓,␈αStanford␈αArtificial
␈↓ α∧␈↓Intelligence Memo 1, Computer Science Department, Stanford University.
␈↓ α∧␈↓␈↓αMcCarthy,␈α∂John␈α∂(1978)␈↓:␈α⊂"Representation␈α∂of␈α∂Recursive␈α∂Programs␈α⊂in␈α∂First␈α∂Order␈α∂Logic",␈α⊂in␈α∂E.K.
␈↓ α∧␈↓Blum␈α
and␈αS.␈α
Takasu␈α(eds.)␈α
␈↓↓Proceedings␈α
of␈αThe␈α
International␈αConference␈α
on␈α
Mathematical␈αStudies
␈↓ α∧␈↓↓of Information Processing␈↓, Kyoto. (a preliminary and superseded version of this paper)
␈↓ α∧␈↓␈↓αMcCarthy, John and Carolyn Talcott (1979)␈↓: ␈↓↓LISP: Programming and Proving␈↓, (in preparation)
␈↓ α∧␈↓␈↓αMorris,␈α∪James␈α∪H.(1968)␈↓:␈α∩␈↓↓Lambda␈α∪Calculus␈α∪Models␈α∩of␈α∪Programming␈α∪Languages␈↓.␈α∪Ph.D.␈α∩Thesis,
␈↓ α∧␈↓M.I.T., Cambridge, Mass.
␈↓ α∧␈↓␈↓αMorris,␈α
James␈αH.,␈α
and␈αBen␈α
Wegbreit␈α
(1977)␈↓:␈α"Program␈α
Verification␈αby␈α
Subgoal␈αInduction",␈α
␈↓↓Comm.
␈↓ α∧␈↓↓ACM␈↓,␈↓α20␈↓(4): 209-222 (April).
␈↓ α∧␈↓␈↓αOppen,␈α∂Derek␈α∂(1978)␈↓:␈α⊂␈↓↓Reasoning␈α∂about␈α∂Recursively␈α⊂Defined␈α∂Data␈α∂Structures␈↓,␈α⊂Stanford␈α∂Artificial
␈↓ α∧␈↓Intelligence Memo 314, Computer Science Department, Stanford University.
␈↓ α∧␈↓␈↓αParis,␈αJeff␈αand␈αLeo␈αHarrington␈α(1977)␈↓:␈α"A␈αMathematical␈αIncompleteness␈αin␈αPeano␈αArithmetic",␈αin
␈↓ α∧␈↓Jon␈α∞Barwise␈α∞(ed.),␈α∂␈↓↓Handbook␈α∞of␈α∞Mathematical␈α∂Logic␈↓,␈α∞pp.␈α∞1133-1142.␈α∂ North-Holland␈α∞Publishing
␈↓ α∧␈↓Company, Amsterdam.
␈↓ α∧␈↓␈↓αPark,␈α_David␈α_(1970)␈↓:␈α_Fixpoint␈α_Induction␈α_and␈α_Proofs␈α_of␈α_Program␈α_Properties",␈α_in␈α↔␈↓↓Machine
␈↓ α∧␈↓↓Intelligence 5␈↓, pp. 59-78, Edinburgh University Press, Edinburgh.
␈↓ α∧␈↓␈↓αScott,␈α∂Dana␈α⊂(1970)␈↓:␈α∂␈↓↓Outline␈α⊂of␈α∂a␈α⊂Mathematical␈α∂Theory␈α⊂of␈α∂Computation␈↓.␈α⊂ Programming␈α∂Research
␈↓ α∧␈↓Group Monograph No. 2, Oxford.
␈↓ α∧␈↓␈↓αTakeuchi, I. (1978)␈↓: Personal Communication.
␈↓ α∧␈↓␈↓αVuillemin,␈α
J.␈α(1973)␈↓:␈α
␈↓↓Proof␈αTechniques␈α
for␈αRecursive␈α
Programs␈↓.␈αPh.D.␈α
Thesis,␈αStanford␈α
University,
␈↓ α∧␈↓Stanford, Calif.